Encoding Agda programs using rewriting

DOI10.4230/LIPICS.FSCD.2020.31MaRDI QIDQ6854402zbMATH OpenFDO

Authors Guillaume Genestier

Publication date 24 February 2026

Copyright license Creative Commons Attribution 3.0 Unported

Full work available at URL https://doi.org/10.4230/LIPICS.FSCD.2020.31

zbMATH Keywords

eta conversionlogical frameworksrewritinguniverse polymorphism

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX) Theory of computing (68Qxx)

Cites work

• A framework for defining logics
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• An induction principle for pure type systems
• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
• scientific article; zbMATH DE number 591911 (Why is no real title available?)
• scientific article; zbMATH DE number 1400716 (Why is no real title available?)
• Sharing a library between proof assistants: reaching out to the HOL family
• Type checking with universes
• Universe polymorphism in Coq

Cited in

(1)

• Encoding of predicate subtyping with proof irrelevance in the -calculus modulo theory

This page was built for publication: Encoding Agda programs using rewriting

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