Publication:5875441
From MaRDI portal
DOI10.4230/LIPIcs.ITP.2019.29MaRDI QIDQ5875441
Publication date: 3 February 2023
Related Items
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Type-based termination of generic programs
- Isabelle/HOL. A proof assistant for higher-order logic
- Truly Modular (Co)datatypes for Isabelle/HOL
- Programming with Higher-Order Logic
- Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving
- The Lean Theorem Prover (System Description)
- First-Class Type Classes
- A Syntax for Higher Inductive-Inductive Types
- The Matita Interactive Theorem Prover
- Canonical Structures for the Working Coq User
- CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions
- Types for Proofs and Programs