Automatically proving equivalence by type-safe reflection

DOI10.1007/978-3-319-62075-6_4MaRDI QIDQ2364699zbMATH OpenOpenAlexFDO

Authors Franck Slama, Edwin Brady

Publication date 21 July 2017

Full work available at URL http://hdl.handle.net/10023/11247

zbMATH Keywords

equivalenceequalityproof automationproof by reflectioncorrect-by-construction softwaretype-driven development

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Auto in Agda. Programming proof search using reflection
• Theorem Proving in Higher Order Logics
• Automation for dependently typed functional programming
• Extensible and efficient automation through reflective tactics
• Dependent types and program equivalence

Cites work

• scientific article; zbMATH DE number 6296049 (Why is no real title available?)
• A proof dedicated meta-language
• Auto in Agda. Programming proof search using reflection
• Compositional computational reflection
• Idris, a general-purpose dependently typed programming language: Design and implementation
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Mtac: a monad for typed tactic programming in Coq
• The formalization of syntax-based mathematical algorithms using quotation and evaluation
• Theorem Proving in Higher Order Logics
• Theorem proving modulo
• Theory presentation combinators
• Types for Proofs and Programs
• Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo

Cited in

(2)

• Proof-relevant Horn clauses for dependent type inference and term synthesis
• scientific article; zbMATH DE number 683355 (Why is no real title available?)

Describes a project that uses

Uses Software

• Idris
• Mtac
• Irdis
• Agda
• Coq

This page was built for publication: Automatically proving equivalence by type-safe reflection

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2364699)