Pages that link to "Item:Q865639"

The following pages link to Innovations in computational type theory using Nuprl (Q865639):

Displaying 21 items.

• Nuprl (Q18826) (← links)
• Intuitionistic completeness of first-order logic (Q392280) (← links)
• Tactics for hierarchical proof (Q626933) (← links)
• Formally computing with the non-computable (Q2117773) (← links)
• A language with type-dependent equality (Q2128827) (← links)
• The effects of effects on constructivism (Q2133168) (← links)
• Implementing Euclid's straightedge and compass constructions in type theory (Q2631963) (← links)
• Nuprl's class theory and its applications (Q2752048) (← links)
• Exercising Nuprl’s Open-Endedness (Q2819194) (← links)
• Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language (Q2947456) (← links)
• ν-Types for Effects and Freshness Analysis (Q3393400) (← links)
• Manifest Fields and Module Mechanisms in Intensional Type Theory (Q3638256) (← links)
• Building Mathematics-Based Software Systems to Advance Science and Create Knowledge (Q3644710) (← links)
• (Q4357062) (← links)
• Validating Brouwer's continuity principle for numbers using named exceptions (Q4640313) (← links)
• (Q5020623) (← links)
• Monotone recursive types and recursive data representations in Cedille (Q5076393) (← links)
• Cartesian cubical computational type theory: Constructive reasoning with paths and equalities (Q5079726) (← links)
• A thorough treatment of highly-efficient NTRU instantiations (Q6091128) (← links)
• Impredicative encodings of inductive-inductive data in Cedille (Q6535795) (← links)
• \(\text{TT}^\Box_{\mathcal{C}}\): a family of extensional type theories with effectful realizers of continuity (Q6597949) (← links)