Jonathan Aldrich, Robert J. Simmons & Key Shin (2008):
SASyLF: An Educational Proof Assistant for Language Theory.
In: International Workshop on Functional and Declarative Programming in Education.
ACM Press,
pp. 31–40,
doi:10.1145/1411260.1411266.
Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich & Steve Zdancewic (2005):
Mechanized Metatheory for the Masses: The PoplMark Challenge.
In: Eighteenth International Conference on Theorem Proving in Higher Order Logics,
LNCS 3603.
Springer,
pp. 50–65,
doi:10.1007/11541868_4.
Christoph Benzmüller, Florian Rabe & Geoff Sutcliffe (2008):
THF0—The Core of the TPTP Language for Higher-Order Logic.
In: Fourth International Joint Conference on Automated Reasoning,
LNCS 5195.
Springer,
pp. 491–506,
doi:10.1007/978-3-540-71070-7_41.
Andrew Cave & Brigitte Pientka (2012):
Programming with Binders and Indexed Data-Types.
In: Thirty-Ninth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.
ACM Press,
pp. 413–424,
doi:10.1145/2103656.2103705.
Matthias Felleisen, Robert Bruce Findler & Matthew Flatt (2009):
Semantics Engineering with PLT Redex.
The MIT Press.
Amy P. Felty & Alberto Momigliano (2012):
Hybrid: A Definitional Two-Level Approach to Reasoning with Higher-Order Abstract Syntax.
Journal of Automated Reasoning 48(1),
pp. 43–105,
doi:10.1007/s10817-010-9194-x.
Amy P. Felty, Alberto Momigliano & Brigitte Pientka (2015):
The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations: Part 1—A Common Infrastructure for Benchmarks.
CoRR abs/1503.06095.
Available at http://arxiv.org/abs/1503.06095.
Amy P. Felty, Alberto Momigliano & Brigitte Pientka (2015):
The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations: Part 2—A Survey.
Journal of Automated Reasoning.
(to appear).
Jean-Christophe Filliâtre (2013):
One Logic To Use Them All.
In: Twenty-Fourth International Conference on Automated Deduction,
LNCS 7898.
Springer,
pp. 1–20,
doi:10.1007/978-3-642-38574-2_1.
Andrew Gacek (2008):
The Abella Interactive Theorem Prover (System Description).
In: Fourth International Joint Conference on Automated Reasoning,
LNCS 5195.
Springer,
pp. 154–161,
doi:10.1007/978-3-540-71070-7_13.
Andrew Gacek, Dale Miller & Gopalan Nadathur (2012):
A Two-Level Logic Approach to Reasoning About Computations.
Journal of Automated Reasoning 49(2),
pp. 241–273,
doi:10.1007/s10817-011-9218-1.
J.-Y. Girard, Y. Lafont & P. Tayor (1990):
Proofs and Types.
Cambridge University Press.
Nada Habli & Amy P. Felty (2013):
Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs.
In: Third International Workshop on Proof Exchange for Theorem Proving,
EasyChair Proceedings in Computing 14,
pp. 67–76.
Holger H. Hoos & Thomas Stützle (2000):
SATLIB: An Online Resource for Research on SAT.
In: SAT 2000: Highlights of Satisfiability Research in the Year 2000,
Frontiers in Artificial Intelligence and Applications 63.
IOS Press,
pp. 283–292.
Alberto Momigliano, Alan J. Martin & Amy P. Felty (2008):
Two-Level Hybrid: A System for Reasoning Using Higher-Order Abstract Syntax.
In: Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2007,
ENTCS 196.
Elsevier,
pp. 85–93,
doi:10.1016/j.entcs.2007.09.019.
Brigitte Pientka (2007):
Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF.
In: Twentieth International Conference on Theorem Proving in Higher-Order Logics,
LNCS.
Springer,
pp. 246–261,
doi:10.1007/978-3-540-74591-4_19.
Brigitte Pientka & Andrew Cave (2015):
Inductive Beluga:Programming Proofs (System Description).
In: Twenty-Fifth International Conference on Automated Deduction.
Springer.
Brigitte Pientka & Joshua Dunfield (2010):
Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description).
In: Fifth International Joint Conference on Automated Reasoning,
LNCS 6173.
Springer,
pp. 15–21,
doi:10.1007/978-3-642-14203-1_2.
Benjamin C. Pierce (2002):
Types and Programming Languages.
MIT Press.
Adam Poswolsky & Carsten Schürmann (2009):
System Description: Delphin—A Functional Programming Language for Deductive Systems.
In: Third International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2008),
ENTCS 228.
Elsevier,
pp. 113–120,
doi:10.1016/j.entcs.2008.12.120.
Florian Rabe & Carsten Schürmann (2009):
A Practical Module System for LF.
In: Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice.
ACM Press,
pp. 40–48,
doi:10.1145/1577824.1577831.
Grigore Roşu & Traian Florin Şerbănuţă (2010):
An Overview of the K Semantic Framework.
Journal of Logic and Algebraic Programming 79(6),
pp. 397–434,
doi:10.1016/j.jlap.2010.03.012.
Carsten Schürmann (2009):
The Twelf Proof Assistant.
In: Twenty-Second International Conference on Theorem Proving in Higher Order Logics,
LNCS 5674.
Springer,
pp. 79–83,
doi:10.1007/978-3-642-03359-9_7.
Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar & Rok Strniša (2010):
Ott: Effective Tool Support for the Working Semanticist.
Journal of Functional Programming 20(1),
pp. 71–122,
doi:10.1017/S0956796809990293.
Geoff Sutcliffe (2009):
The TPTP Problem Library and Associated Infrastructure.
Journal of Automated Reasoning 43(4),
pp. 337–362,
doi:10.1007/s10817-009-9143-8.
Yuting Wang, Kaustuv Chaudhuri, Andrew Gacek & Gopalan Nadathur (2013):
Reasoning About Higher-Order Relational Specifications.
In: Fifteenth International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming.
ACM Press,
pp. 157–168,
doi:10.1145/2505879.2505889.