Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules

DOI10.4230/lipics.types.2019.2OpenAlexW3095227982MaRDI QIDQ6079228

Jesper Cockx

Publication date: 27 October 2023

Full work available at URL: https://drops.dagstuhl.de/opus/volltexte/2020/13066/pdf/LIPIcs-TYPES-2019-2.pdf/

zbMATH Keywords

dependent typeshigher-order rewritingAgdaproof assistantsrewrite rules

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

Calculating datastructures

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Higher-order rewrite systems and their confluence
• Maude: specification and programming in rewriting logic
• Failure is not an option. An exceptional type theory
• Programming up to Congruence
• Coq Modulo Theory
• Towards Rewriting in Coq
• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• A framework for defining logics
• Modularity of strong normalization in the algebraic-λ-cube
• Termination of rewriting in the Calculus of Constructions
• Coq without Type Casts: A Complete Proof of Coq Modulo Theory
• Definitions by rewriting in the Calculus of Constructions
• Overlapping and Order-Independent Patterns
• Types for Proofs and Programs
• Consistency and Completeness of Rewriting in the Calculus of Constructions

This page was built for publication: Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules