Pages that link to "Item:Q5887516"
From MaRDI portal
The following pages link to Inductively defined types in the Calculus of Constructions (Q5887516):
Displaying 7 items.
- Metacircularity in the polymorphic \(\lambda\)-calculus (Q1177938) (← links)
- A note on complexity measures for inductive classes in constructive type theory (Q1271558) (← links)
- Cut elimination for a logic with induction and co-induction (Q1948276) (← links)
- Deciding Kleene algebra terms equivalence in Coq (Q2347910) (← links)
- From realizability to induction via dependent intersection (Q2636522) (← links)
- A henkin-style completeness proof for the modal logic S5 (Q2695534) (← links)
- The formal verification of the ctm approach to forcing (Q6151819) (← links)
