Inductive beluga: programming proofs

DOI10.1007/978-3-319-21401-6_18MaRDI QIDQ3454100zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

dependent typeslogical frameworksproof assistant

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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

Cites work

• A framework for defining logics
• A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
• An insider's look at LF type reconstruction: everything you (n)ever wanted to know
• Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
• Case analysis of higher-order data
• Contextual modal type theory
• Intensional interpretations of functionals of finite type I
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Programming type-safe transformations using higher-order abstract syntax
• Programming with binders and indexed data-types
• The Abella Interactive Theorem Prover (System Description)
• The Alf proof editor and its proof engine
• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• Well-founded recursion over contextual objects

Cited in

(13)

• Programs using syntax with first-class binders
• 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
• scientific article; zbMATH DE number 7204440 (Why is no real title available?)
• 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

Describes a project that uses

Uses Software

• Abella
• ALF
• Twelf
• Beluga

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)