Inductive beluga: programming proofs
From MaRDI portal
Publication:3454100
DOI10.1007/978-3-319-21401-6_18zbMATH Open1465.68294OpenAlexW1433844459MaRDI QIDQ3454100FDOQ3454100
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
- Title not available (Why is that?)
- 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 (8)
- A case study in programming coinductive proofs: Howe’s method
- Lexicographic Path Induction
- Programs Using Syntax with First-Class Binders
- LINCX: A Linear Logical Framework with First-Class Contexts
- Title not available (Why is that?)
- Harpoon: mechanizing metatheory interactively
- Semantical analysis of contextual types
- Title not available (Why is that?)
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)
