Codifying guarded definitions with recursive schemes

DOI10.1007/3-540-60579-7_3zbMath1530.03054OpenAlexW1980786790MaRDI QIDQ6083895

Unnamed Author

Publication date: 8 December 2023

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

Full work available at URL: https://doi.org/10.1007/3-540-60579-7_3

zbMATH Keywords

proof systemcase analysisreduction rulerecursive calltyping rule

Mathematics Subject Classification ID

Logic in computer science (03B70) Mechanization of proofs and logical operations (03B35) Formalization of mathematics in connection with theorem provers (68V20) Type theory (03B38)

Related Items (5)

Turing-Completeness Totally Free ⋮ Quotients by Idempotent Functions in Cedille ⋮ Unnamed Item ⋮ Friends with Benefits ⋮ Undecidability of equality for codata types

Cites Work

• Unnamed Item
• Unnamed Item
• A co-induction principle for recursively defined domains
• Introduction to generalized type systems

This page was built for publication: Codifying guarded definitions with recursive schemes