Automatically proving equivalence by type-safe reflection

DOI10.1007/978-3-319-62075-6_4zbMath1367.68257OpenAlexW2728028396MaRDI QIDQ2364699

Edwin Brady, Franck Slama

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)

Related Items (1)

Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis

Uses Software

• Coq
• Agda
• Irdis
• Mtac
• Idris

Cites Work

• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Theorem proving modulo
• The Formalization of Syntax-Based Mathematical Algorithms Using Quotation and Evaluation
• Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo
• Compositional Computational Reflection
• Theory Presentation Combinators
• Auto in Agda
• Mtac
• Idris, a general-purpose dependently typed programming language: Design and implementation
• Theorem Proving in Higher Order Logics
• Types for Proofs and Programs

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