• Momigliano A and Sassella M. (2024). More Church-Rosser Proofs in BELUGA. Electronic Proceedings in Theoretical Computer Science. 10.4204/EPTCS.402.6. 402. (34-42).

    http://arxiv.org/abs/2404.14921v1

  • Sato M, Pollack R, Schwichtenberg H and Sakurai T. (2013). Viewing -terms through maps . Indagationes Mathematicae. 10.1016/j.indag.2013.08.003. 24:4. (1073-1104). Online publication date: 1-Nov-2013.

    https://linkinghub.elsevier.com/retrieve/pii/S0019357713000633

  • Accattoli B. Proof Pearl: Abella Formalization of λ-Calculus Cube Property. Certified Programs and Proofs. (173-187).

    https://doi.org/10.1007/978-3-642-35308-6_15

  • Vouillon J. (2011). A Solution to the PoplMark Challenge Based on de Bruijn Indices. Journal of Automated Reasoning. 10.1007/s10817-011-9230-5. 49:3. (327-362). Online publication date: 1-Oct-2012.

    http://link.springer.com/10.1007/s10817-011-9230-5

  • Shankar N and Vaucher M. (2011). The Mechanical Verification of a DPLL-Based Satisfiability Solver. Electronic Notes in Theoretical Computer Science (ENTCS). 269:C. (3-17). Online publication date: 22-Apr-2011.

    /doi/10.5555/2952797.2952916

  • Shankar N and Vaucher M. (2011). The Mechanical Verification of a DPLL-Based Satisfiability Solver. Electronic Notes in Theoretical Computer Science. 10.1016/j.entcs.2011.03.002. 269. (3-17). Online publication date: 1-Apr-2011.

    http://linkinghub.elsevier.com/retrieve/pii/S1571066111000594

  • Galdino A and Ayala-Rincón M. (2010). A Formalization of the Knuth---Bendix(---Huet) Critical Pair Theorem. Journal of Automated Reasoning. 45:3. (301-325). Online publication date: 1-Oct-2010.

    https://doi.org/10.1007/s10817-010-9165-2

  • Aydemir B, Charguéraud A, Pierce B, Pollack R and Weirich S. (2008). Engineering formal metatheory. ACM SIGPLAN Notices. 43:1. (3-15). Online publication date: 14-Jan-2008.

    https://doi.org/10.1145/1328897.1328443

  • Aydemir B, Charguéraud A, Pierce B, Pollack R and Weirich S. Engineering formal metatheory. Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. (3-15).

    https://doi.org/10.1145/1328438.1328443

  • Norrish M and Vestergaard R. Proof pearl. Proceedings of the 20th international conference on Theorem proving in higher order logics. (207-222).

    /doi/10.5555/1792233.1792249

  • Norrish M and Vestergaard R. Proof Pearl: De Bruijn Terms Really Do Work. Theorem Proving in Higher Order Logics. 10.1007/978-3-540-74591-4_16. (207-222).

    http://link.springer.com/10.1007/978-3-540-74591-4_16

  • Struth G. (2006). Abstract abstract reduction. The Journal of Logic and Algebraic Programming. 10.1016/j.jlap.2005.04.001. 66:2. (239-270). Online publication date: 1-Feb-2006.

    http://linkinghub.elsevier.com/retrieve/pii/S1567832605000391

  • Simpson C. (2004). Computer Theorem Proving in Mathematics. Letters in Mathematical Physics. 10.1007/s11005-004-0607-9. 69:1-3. (287-315). Online publication date: 1-Jul-2004.

    http://link.springer.com/10.1007/s11005-004-0607-9

  • Vestergaard R and Brotherston J. (2003). A formalised first-order confluence proof for the λ-calculus using one-sorted variable names. Information and Computation. 183:2. (212-244). Online publication date: 15-Jun-2003.

    https://doi.org/10.1016/S0890-5401(03)00023-3

  • Belinfante J. (2003). Reasoning about Iteration in Gödel’s Class Theory. Automated Deduction – CADE-19. 10.1007/978-3-540-45085-6_18. (228-242).

    https://link.springer.com/10.1007/978-3-540-45085-6_18

  • Ruiz-Reina J, Alonso J, Hidalgo M and Martín-Mateos F. (2002). Formal Proofs About Rewriting Using ACL2. Annals of Mathematics and Artificial Intelligence. 36:3. (239-262). Online publication date: 25-Nov-2002.

    https://doi.org/10.1023/A:1016003314081

  • Struth G. (2002). Calculating Church-Rosser Proofs in Kleene Algebra. Relational Methods in Computer Science. 10.1007/3-540-36280-0_19. (276-290).

    http://link.springer.com/10.1007/3-540-36280-0_19

  • Abel A. (2001). A Third-Order Representation of the λμ-Calculus. Electronic Notes in Theoretical Computer Science. 10.1016/S1571-0661(04)00281-6. 58:1. (97-114). Online publication date: 1-Nov-2001.

    http://linkinghub.elsevier.com/retrieve/pii/S1571066104002816

  • Vestergaard R and Brotherston J. (2001). The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective). Electronic Notes in Theoretical Computer Science. 10.1016/S1571-0661(04)00277-4. 58:1. (18-36). Online publication date: 1-Nov-2001.

    http://linkinghub.elsevier.com/retrieve/pii/S1571066104002774

  • Struth G. Calculating Church-Rosser Proofs in Kleene Algebra. Revised Papers from the 6th International Conference and 1st Workshop of COST Action 274 TARSKI on Relational Methods in Computer Science. (276-290).

    /doi/10.5555/646681.702460

  • Pfenning F. Logical frameworks. Handbook of automated reasoning. (1063-1147).

    /doi/10.5555/778522.778526

  • Giesl J. (2001). Induction Proofs with Partial Functions. Journal of Automated Reasoning. 26:1. (1-49). Online publication date: 1-Jan-2001.

    https://doi.org/10.1023/A:1006408829523

  • Ford J and Mason I. (2001). Operational Techniques in PVS — A Preliminary Evaluation. Electronic Notes in Theoretical Computer Science. 10.1016/S1571-0661(04)80882-X. 42. (124-142). Online publication date: 1-Jan-2001.

    http://linkinghub.elsevier.com/retrieve/pii/S157106610480882X

  • Pfenning F. (2001). Logical Frameworks. Handbook of Automated Reasoning. 10.1016/B978-044450813-3/50019-9. (1063-1147).

    http://linkinghub.elsevier.com/retrieve/pii/B9780444508133500199

  • Vestergaard R and Brotherston J. (2001). A Formalised First-Order Con uence Proof for the λ-Calculus Using One-Sorted Variable Names (Barendregt Was Right after all ... almost). Rewriting Techniques and Applications. 10.1007/3-540-45127-7_23. (306-321).

    http://link.springer.com/10.1007/3-540-45127-7_23

  • Ruiz-Reina J, Alonso J, Hidalgo M and Martín-Mateos F. (2001). Formalizing Rewriting in the ACL2 Theorem Prover. Artificial Intelligence and Symbolic Computation. 10.1007/3-540-44990-6_7. (92-106).

    http://link.springer.com/10.1007/3-540-44990-6_7

  • Mckinna J and Pollack R. (1999). Some Lambda Calculus and Type Theory Formalized. Journal of Automated Reasoning. 23:3. (373-409). Online publication date: 1-Nov-1999.

    https://doi.org/10.1023/A:1006294005493

  • Goldschlag D. (1999). A Mechanization of Unity in PC-NQTHM-92. Journal of Automated Reasoning. 23:3. (445-498). Online publication date: 1-Nov-1999.

    https://doi.org/10.1023/A:1006262609127

  • Giunchiglia F, Bertoli P and Coglio A. (1998). The OMRS Project: State of the Art. Electronic Notes in Theoretical Computer Science. 10.1016/S1571-0661(05)82556-3. 15. (127-146).

    http://linkinghub.elsevier.com/retrieve/pii/S1571066105825563

  • Basin D and Matthews S. (1998). Scoped Metatheorems. Electronic Notes in Theoretical Computer Science. 10.1016/S1571-0661(05)80021-0. 15. (353-366).

    http://linkinghub.elsevier.com/retrieve/pii/S1571066105800210

  • Jantzen M. (1997). Basics of Term Rewriting. Handbook of Formal Languages. 10.1007/978-3-642-59126-6_5. (269-337).

    http://link.springer.com/10.1007/978-3-642-59126-6_5

  • Kaufmann M and Strother Moore J. ACL2: an industrial strength version of Nqthm 11th Annual Conference on Computer Assurance. COMPASS '96. 10.1109/CMPASS.1996.507872. 0-7803-3390-X. (23-34).

    http://ieeexplore.ieee.org/document/507872/

  • Pfenning F. (1996). The practice of logical frameworks. Trees in Algebra and Programming — CAAP '96. 10.1007/3-540-61064-2_33. (119-134).

    http://link.springer.com/10.1007/3-540-61064-2_33

  • Boyer R, Kaufmann M and Moore J. (1995). The Boyer-Moore theorem prover and its interactive enhancement. Computers & Mathematics with Applications. 10.1016/0898-1221(94)00215-7. 29:2. (27-62). Online publication date: 1-Jan-1995.

    http://linkinghub.elsevier.com/retrieve/pii/0898122194002157

  • Goldschlag D. (1994). Mechanically verifying safety and liveness properties of delay insensitive circuits. Formal Methods in System Design. 5:3. (207-225). Online publication date: 1-Dec-1994.

    https://doi.org/10.1007/BF01383831

  • Gordon A. (1994). A mechanisation of name-carrying syntax up to alpha-conversion. Higher Order Logic Theorem Proving and Its Applications. 10.1007/3-540-57826-9_152. (413-425).

    http://link.springer.com/10.1007/3-540-57826-9_152

  • Ohtsuka H. (1993). A proof of the substitution lemma in de Bruijn's notation. Information Processing Letters. 46:2. (63-66). Online publication date: 17-May-1993.

    https://doi.org/10.1016/0020-0190(93)90198-I

  • Goldschlag D. (1990). Mechanically Verifying Concurrent Programs with the Boyer-Moore Prove. IEEE Transactions on Software Engineering. 16:9. (1005-1023). Online publication date: 1-Sep-1990.

    https://doi.org/10.1109/32.58787

  • (2009). Books. Artificial Intelligence for Engineering, Design, Analysis and Manufacturing. 10.1017/S0890060400001165. 3:02. (137). Online publication date: 1-May-1989.

    http://www.journals.cambridge.org/abstract_S0890060400001165