Pages that link to "Item:Q5887516"

The following pages link to Inductively defined types in the Calculus of Constructions (Q5887516):

Displaying 24 items.

• Metacircularity in the polymorphic \(\lambda\)-calculus (Q1177938) (← links)
• A note on complexity measures for inductive classes in constructive type theory (Q1271558) (← links)
• A construction method for induced types and its application to \(G_2\) (Q1283671) (← links)
• Total objects in inductively defined types (Q1374674) (← links)
• Construction of tame types (Q1728696) (← 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)
• Refining inductive types (Q2890506) (← links)
• Denotational cost semantics for functional languages with inductive types (Q2981951) (← links)
• Inductive Type Schemas as Functors (Q3434680) (← links)
• Dual Calculus with Inductive and Coinductive Types (Q3636828) (← links)
• (Q4457447) (← links)
• (Q4508290) (← links)
• (Q4681362) (← links)
• (Q5014449) (← links)
• Monotone recursive definition of predicates and its realizability interpretation (Q5096211) (← links)
• Type Theories from Barendregt’s Cube for Theorem Provers (Q5251190) (← links)
• Type-Based Productivity of Stream Definitions in the Calculus of Constructions (Q5271060) (← links)
• The calculus of dependent lambda eliminations (Q5372010) (← links)
• Least and greatest fixed points in intuitionistic natural deduction (Q5958300) (← links)
• The formal verification of the ctm approach to forcing (Q6151819) (← links)
• Builtin types viewed as inductive families (Q6535230) (← links)