Inductive Beluga: Programming Proofs
From MaRDI portal
Publication:3454100
DOI10.1007/978-3-319-21401-6_18zbMath1465.68294OpenAlexW1433844459MaRDI QIDQ3454100
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
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (7)
Semantical analysis of contextual types ⋮ Unnamed Item ⋮ Programs Using Syntax with First-Class Binders ⋮ LINCX: A Linear Logical Framework with First-Class Contexts ⋮ Unnamed Item ⋮ Harpoon: mechanizing metatheory interactively ⋮ A case study in programming coinductive proofs: Howe’s method
Uses Software
Cites Work
- Unnamed Item
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
- 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
- Programming Type-Safe Transformations Using Higher-Order Abstract Syntax
- Programming with binders and indexed data-types
- A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
- The Abella Interactive Theorem Prover (System Description)
- A framework for defining logics
- An insider's look at LF type reconstruction: everything you (n)ever wanted to know
- Contextual modal type theory
- Intensional interpretations of functionals of finite type I
- Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
- The Alf proof editor and its proof engine
This page was built for publication: Inductive Beluga: Programming Proofs
