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.
Stefano Berardi (1990):
Girard Normalization Proof in LEGO.
In: Proceedings of the First Workshop on Logical Frameworks,
pp. 67–78.
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.
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.
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.
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.
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.
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.
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.
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.
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.
J.-Y. Girard, Y. Lafont & P. Tayor (1990):
Proofs and types.
Cambridge University Press.
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.
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.
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.
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.
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.
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.
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.
Brigitte Pientka & Andrew Cave (2015):
Inductive Beluga:Programming Proofs (System description).
In: 25th International Conference on Automated Deduction (CADE-25).
Springer.
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.
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.
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.
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.
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.
William Tait (1967):
Intensional Interpretations of Functionals of Finite Type I.
J. Symb. Log. 32(2),
pp. 198–212,
doi:10.2307/2271658.
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.