Inductive beluga: programming proofs
DOI10.1007/978-3-319-21401-6_18zbMATH Open1465.68294OpenAlexW1433844459MaRDI QIDQ3454100FDOQ3454100
Authors: Brigitte Pientka, Andrew Cave 
Publication date: 2 December 2015
Published in: Automated Deduction - CADE-25 (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-21401-6_18
Recommendations
- Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
- Programming inductive proofs. A new approach based on contextual types
- Mechanizing proofs with logical relations -- Kripke-style
- A case study in programming coinductive proofs: Howe's method
- POPLMark reloaded: mechanizing proofs by logical relations
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
- The Abella Interactive Theorem Prover (System Description)
- A framework for defining logics
- Contextual modal type theory
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Case analysis of higher-order data
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
- Programming with binders and indexed data-types
- A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
- Well-founded recursion over contextual objects
- Intensional interpretations of functionals of finite type I
- An insider's look at LF type reconstruction: everything you (n)ever wanted to know
- Programming type-safe transformations using higher-order abstract syntax
- The Alf proof editor and its proof engine
Cited In (13)
- Plugging-in proof development environments using \textit{locks} in \(\mathsf{LF}\)
- \textsc{Lincx}: a linear logical framework with first-class contexts
- Lexicographic Path Induction
- Meta-theory à la carte
- Formalized proof systems for propositional logic
- A case study in programming coinductive proofs: Howe's method
- Title not available (Why is that?)
- Programming inductive proofs. A new approach based on contextual types
- POPLMark reloaded: mechanizing proofs by logical relations
- Mechanizing proofs with logical relations -- Kripke-style
- Harpoon: mechanizing metatheory interactively
- Semantical analysis of contextual types
- Programs using syntax with first-class binders
Uses Software
This page was built for publication: Inductive beluga: programming proofs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3454100)
