The Abella Interactive Theorem Prover (System Description)
- 29 August 2008
- book chapter
- conference paper
- Published by Springer Science and Business Media LLC in Lecture Notes in Computer Science
Abstract
No abstract availableKeywords
Other Versions
This publication has 11 references indexed in Scilit:
- Least and Greatest Fixed Points in Linear LogicPublished by Springer Science and Business Media LLC ,2007
- A proof theory for generic judgmentsACM Transactions on Computational Logic, 2005
- Mechanized Metatheory for the Masses: The PoplMark ChallengeLecture Notes in Computer Science, 2005
- Practical Higher-Order Pattern Unification with On-the-Fly RaisingLecture Notes in Computer Science, 2005
- Reasoning with higher-order abstract syntax in a logical frameworkACM Transactions on Computational Logic, 2002
- Abstract Syntax for Variable Binders: An OverviewLecture Notes in Computer Science, 2000
- System Description: Teyjus—A Compiler and Abstract Machine Based Implementation of λPrologLecture Notes in Computer Science, 1999
- System Description: Twelf — A Meta-Logical Framework for Deductive SystemsLecture Notes in Computer Science, 1999
- Uniform proofs as a foundation for logic programmingAnnals of Pure and Applied Logic, 1991
- Intensional interpretations of functionals of finite type IThe Journal of Symbolic Logic, 1967