The following pages link to (Q4099613):
Displaying 50 items.
- Normalization by evaluation and algebraic effects (Q265792) (← links)
- Category theory, logic and formal linguistics: some connections, old and new (Q280832) (← links)
- Apartness spaces and uniform neighbourhood structures (Q290645) (← links)
- Martin-Löf complexes (Q385803) (← links)
- A scalable module system (Q391632) (← links)
- Intuitionistic completeness of first-order logic (Q392280) (← links)
- Constructivist and structuralist foundations: Bishop's and Lawvere's theories of sets (Q448334) (← links)
- Coalgebras in functional programming and type theory (Q639643) (← links)
- Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation (Q651316) (← links)
- Representing model theory in a type-theoretical logical framework (Q654913) (← links)
- Adjectival and adverbial modification: the view from modern type theories (Q683682) (← links)
- Type-theoretic interpretation of iterated, strictly positive inductive definitions (Q688845) (← links)
- Isomorphism is equality (Q740487) (← links)
- Equational type logic (Q752689) (← links)
- Realizability and intuitionistic logic (Q792319) (← links)
- Propositions and specifications of programs in Martin-Löf's type theory (Q800719) (← links)
- Innovations in computational type theory using Nuprl (Q865639) (← links)
- Meta-circular interpreter for a strongly typed language (Q908683) (← links)
- Proof-theoretical analysis: Weak systems of functions and classes (Q911585) (← links)
- Constructive system for automatic program synthesis (Q912589) (← links)
- Continuity and Lipschitz constants for projections (Q1044668) (← links)
- Programs as proofs: A synopsis (Q1051424) (← links)
- A proof description language and its reduction system (Q1055769) (← links)
- A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction (Q1075050) (← links)
- On the syntax of Martin-Löf's type theories (Q1099173) (← links)
- Pebble, a kernel language for modules and abstract data types (Q1104071) (← links)
- The calculus of constructions (Q1108266) (← links)
- On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory (Q1120558) (← links)
- Generalization from partial parametrization in higher-order type theory (Q1122980) (← links)
- Type checking with universes (Q1177937) (← links)
- Proof normalization with nonstandard objects (Q1178706) (← links)
- An intuitionistic theory of types with assumptions of high-arity variables (Q1192333) (← links)
- Map theory (Q1193653) (← links)
- Constructing type systems over an operational semantics (Q1199709) (← links)
- Coquand's calculus of constructions: A mathematical foundation for a proof development system (Q1201296) (← links)
- From constructivism to computer science (Q1274450) (← links)
- Constructive mathematics: a foundation for computable analysis (Q1292399) (← links)
- Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\) (Q1295369) (← links)
- Well-ordering proofs for Martin-Löf type theory (Q1295372) (← links)
- Inaccessibility in constructive set theory and type theory (Q1295396) (← links)
- Inductive families (Q1336951) (← links)
- A constructive valuation semantics for classical logic (Q1355127) (← links)
- Induction-recursion and initial algebras. (Q1412830) (← links)
- Proof-search in type-theoretic languages: An introduction (Q1575935) (← links)
- Meaning explanations at higher dimension (Q1688954) (← links)
- To be or not to be constructive, that is not the question (Q1688964) (← links)
- Independence results around constructive ZF (Q1765158) (← links)
- Univalence as a principle of logic (Q1788330) (← links)
- Combinatorial topology and constructive mathematics (Q1788338) (← links)
- Towards a computation system based on set theory (Q1825191) (← links)
