Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
- 1 January 2010
- conference paper
- conference paper
- Published by Springer Science and Business Media LLC in Lecture Notes in Computer Science
Abstract
No abstract availableThis publication has 9 references indexed in Scilit:
- The Abella Interactive Theorem Prover (System Description)Lecture Notes in Computer Science, 2008
- Programming with proofs and explicit contextsPublished by Association for Computing Machinery (ACM) ,2008
- A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutionsPublished by Association for Computing Machinery (ACM) ,2008
- Verifying Termination and Reduction Properties about Higher-Order Logic ProgramsJournal of Automated Reasoning, 2005
- System Description: Twelf — A Meta-Logical Framework for Deductive SystemsLecture Notes in Computer Science, 1999
- Proof-carrying codePublished by Association for Computing Machinery (ACM) ,1997
- Mode and termination checking for higher-order logic programsLecture Notes in Computer Science, 1996
- A framework for defining logicsJournal of the ACM, 1993
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple UnificationJournal of Logic and Computation, 1991