Automatically proving equivalence by type-safe reflection

DOI10.1007/978-3-319-62075-6_4zbMATH Open1367.68257OpenAlexW2728028396MaRDI QIDQ2364699FDOQ2364699

Authors: Franck Slama, Edwin Brady 

Publication date: 21 July 2017

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

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

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)

Cites Work

• Title not available (Why is that?)
• Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo
• Mtac: a monad for typed tactic programming in Coq
• 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.
• Theorem Proving in Higher Order Logics
• Theorem proving modulo
• The formalization of syntax-based mathematical algorithms using quotation and evaluation
• A proof dedicated meta-language
• Theory presentation combinators
• Compositional computational reflection
• Auto in Agda. Programming proof search using reflection
• Types for Proofs and Programs

Cited In (2)

• Proof-relevant Horn clauses for dependent type inference and term synthesis
• Title not available (Why is that?)

Uses Software

• Coq
• Agda
• Irdis
• Mtac
• Idris

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)