References

  1. Thorsten Altenkirch (1993): A Formalization of the Strong Normalization Proof for System F in LEGO. In: Marc Bezem & Jan Friso Groote: International Conference on Typed Lambda Calculi and Applications (TLCA '93), Lecture Notes in Computer Science 664. Springer, pp. 13–28, doi:10.1007/BFb0037095.
  2. Stefano Berardi (1990): Girard Normalization Proof in LEGO. In: Proceedings of the First Workshop on Logical Frameworks, pp. 67–78.
  3. Andrew Cave & Brigitte Pientka (2012): Programming with binders and indexed data-types. In: 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'12). ACM Press, pp. 413–424, doi:10.1145/2103656.2103705.
  4. Andrew Cave & Brigitte Pientka (2013): First-class substitutions in contextual type theory. In: Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'13). ACM Press, pp. 15–24, doi:10.1145/2503887.2503889.
  5. Catarina Coquand (1992): A proof of normalization for simply typed lambda calculus writting in ALF. In: Informal Proceedings of Workshop on Types for Proofs and Programs. Dept. of Computing Science, Chalmers Univ. of Technology and Göteborg Univ., pp. 80–87.
  6. Karl Crary (2005): Logical Relations and a Case Study in Equivalence Checking. In: Bejamin C. Pierce: Advanced Topics in Types and Programming Languages. The MIT Press.
  7. Christian Doczkal & Jan Schwinghammer (2009): Formalizing a Strong Normalization Proof for Moggi's Computational Metalanguage: A Case Study in Isabelle/HOL-nominal. In: Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'09). ACM, pp. 57–63, doi:10.1145/1577824.1577834.
  8. Amy Felty & Alberto Momigliano (2012): Hybrid - A Definitional Two-Level Approach to Reasoning with Higher-Order Abstract Syntax. J. Autom. Reasoning 48(1), pp. 43–105, doi:10.1007/s10817-010-9194-x.
  9. Andrew Gacek (2008): The Abella Interactive Theorem Prover (System Description). In: 4th International Joint Conference on Automated Reasoning, Lecture Notes in Artificial Intelligence 5195. Springer, pp. 154–161, doi:10.1007/978-3-540-71070-7_13.
  10. Andrew Gacek, Dale Miller & Gopalan Nadathur (2008): Combining generic judgments with recursive definitions. In: F. Pfenning: 23rd Symposium on Logic in Computer Science. IEEE Computer Society Press, pp. 33–44, doi:10.1109/LICS.2008.33.
  11. Andrew Gacek, Dale Miller & Gopalan Nadathur (2009): Reasoning in Abella about Structural Operational Semantics Specifications. In: Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice (LFMTP 2008), Electronic Notes in Theoretical Computer Science (ENTCS) 228. Elsevier, pp. 85 – 100, doi:10.1016/j.entcs.2008.12.118.
  12. J.-Y. Girard, Y. Lafont & P. Tayor (1990): Proofs and types. Cambridge University Press.
  13. Robert Harper, Furio Honsell & Gordon Plotkin (1993): A Framework for Defining Logics. Journal of the ACM 40(1), pp. 143–184, doi:10.1145/138027.138060.
  14. Robert Harper & Frank Pfenning (2005): On Equivalence and Canonical Forms in the LF Type Theory. ACM Transactions on Computational Logic 6(1), pp. 61–101, doi:10.1145/1042038.1042041.
  15. Aleksandar Nanevski, Frank Pfenning & Brigitte Pientka (2008): Contextual modal type theory. ACM Transactions on Computational Logic 9(3), pp. 1–49, doi:10.1145/1352582.1352591.
  16. Julien Narboux & Christian Urban (2008): Formalising in Nominal Isabelle Crary's Completeness Proof for Equivalence Checking. Electr. Notes Theor. Comput. Sci. 196, pp. 3–18, doi:10.1016/j.entcs.2007.09.014.
  17. Frank Pfenning & Carsten Schürmann (1999): System Description: Twelf — A Meta-Logical Framework for Deductive Systems. In: H. Ganzinger: 16th International Conference on Automated Deduction (CADE-16), Lecture Notes in Artificial Intelligence (LNAI 1632). Springer, pp. 202–206, doi:10.1007/3-540-48660-7_14.
  18. Brigitte Pientka (2008): A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In: 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'08). ACM Press, pp. 371–382, doi:10.1145/1328438.1328483.
  19. Brigitte Pientka & Andreas Abel (2015): Structural Recursion over Contextual Objects. In: Thorsten Altenkirch: 13th International Conference on Typed Lambda Calculi and Applications (TLCA'15). Leibniz International Proceedings in Informatics (LIPIcs) of Schloss Dagstuhl, pp. 273–287, doi:10.4230/LIPIcs.TLCA.2015.273.
  20. Brigitte Pientka & Andrew Cave (2015): Inductive Beluga:Programming Proofs (System description). In: 25th International Conference on Automated Deduction (CADE-25). Springer.
  21. Brigitte Pientka & Joshua Dunfield (2008): Programming with proofs and explicit contexts. In: ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'08). ACM Press, pp. 163–173, doi:10.1145/1389449.1389469.
  22. Brigitte Pientka & Joshua Dunfield (2010): Beluga: a Framework for Programming and Reasoning with Deductive Systems (System Description). In: Jürgen Giesl & Reiner Haehnle: 5th International Joint Conference on Automated Reasoning (IJCAR'10), Lecture Notes in Artificial Intelligence (LNAI 6173). Springer-Verlag, pp. 15–21, doi:10.1007/978-3-642-14203-1_2.
  23. Adam B. Poswolsky & Carsten Schürmann (2008): Practical programming with higher-order encodings and dependent types. In: 17th European Symposium on Programming (ESOP '08) 4960. Springer, pp. 93–107, doi:10.1007/978-3-540-78739-6_7.
  24. Ulrik Rasmussen & Andrzej Filinski (2013): Structural Logical Relations with Case Analysis and Equality Reasoning. In: Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP'13). ACM Press, pp. 43–54, doi:10.1145/2503887.2503891.
  25. Carsten Schürmann & Jeffrey Sarnat (2008): Structural Logical Relations. In: 23rd Annual Symposium on Logic in Computer Science (LICS), Pittsburgh, PA, USA. IEEE Computer Society, pp. 69–80, doi:10.1109/LICS.2008.44.
  26. William Tait (1967): Intensional Interpretations of Functionals of Finite Type I. J. Symb. Log. 32(2), pp. 198–212, doi:10.2307/2271658.
  27. Christian Urban, James Cheney & Stefan Berghofer (2011): Mechanizing the metatheory of LF. ACM Trans. Comput. Log. 12(2), pp. 15, doi:10.1145/1877714.1877721.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org