Auto in Agda. Programming proof search using reflection

DOI10.1007/978-3-319-19797-5_14MaRDI QIDQ2941181zbMATH OpenOpenAlexFDO

Authors Pepijn Kokke, Wouter Swierstra

Publication date 27 August 2015

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-19797-5_14

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• How to make ad hoc proof automation less ad hoc
• How to make ad hoc proof automation less ad hoc
• Types for Proofs and Programs
• Extensible and efficient automation through reflective tactics
• scientific article; zbMATH DE number 1614692

Cites work

• scientific article; zbMATH DE number 1952947 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• scientific article; zbMATH DE number 6296049 (Why is no real title available?)
• A library for polymorphic dynamic typing
• Compositional computational reflection
• Dependently typed programming in Agda
• First-order unification by structural recursion
• Idris, a general-purpose dependently typed programming language: Design and implementation
• MetaML and multi-stage programming with explicit annotations
• More dependent types for distributed arrays
• Mtac: a monad for typed tactic programming in Coq
• The power of Pi
• Typed syntactic meta-programming
• Types for Proofs and Programs

Cited in

(13)

• Types for Proofs and Programs
• Proof-relevant Horn clauses for dependent type inference and term synthesis
• How to make ad hoc proof automation less ad hoc
• Automation for dependently typed functional programming
• -Ware: hardware description and verification in Agda
• Automatically proving equivalence by type-safe reflection
• Elaborator reflection: extending Idris in Idris
• Counterpart-based quantified temporal logics
• Lightweight proof by reflection using a posteriori simulation of effectful computation
• Combining interactive and automatic reasoning in first order theories of functional programs
• Meta programming on the proof level
• Specification and verification of a linear-time temporal logic for graph transformation
• Extensible and efficient automation through reflective tactics

Describes a project that uses

Uses Software

• Mtac
• Agda
• Coq

This page was built for publication: Auto in Agda. Programming proof search using reflection

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