Auto in Agda

DOI10.1007/978-3-319-19797-5_14zbMath1432.68063OpenAlexW759633442MaRDI QIDQ2941181

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)

Related Items (3)

Automatically proving equivalence by type-safe reflection ⋮ Extensible and Efficient Automation Through Reflective Tactics ⋮ Unnamed Item

Uses Software

• Coq
• Agda
• Mtac

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• MetaML and multi-stage programming with explicit annotations
• More dependent types for distributed arrays
• Compositional Computational Reflection
• First-order unification by structural recursion
• Dependently Typed Programming in Agda
• The power of Pi
• Typed syntactic meta-programming
• Mtac
• Idris, a general-purpose dependently typed programming language: Design and implementation
• A library for polymorphic dynamic typing
• Types for Proofs and Programs

This page was built for publication: Auto in Agda