Pages that link to "Item:Q3343983"
From MaRDI portal
The following pages link to Constructive mathematics and computer programming (Q3343983):
Displaying 44 items.
- Extended bar induction in applicative theories (Q753810) (← links)
- Functorial polymorphism (Q753948) (← links)
- Innovations in computational type theory using Nuprl (Q865639) (← links)
- The Girard-Reynolds isomorphism (second edition) (Q879366) (← links)
- Proof-theoretical analysis: Weak systems of functions and classes (Q911585) (← links)
- Do-it-yourself type theory (Q911744) (← links)
- Domain interpretations of Martin-Löf's partial type theory (Q916656) (← links)
- HasCasl: integrated higher-order specification and program development (Q1006648) (← links)
- Possible forms of evaluation or reduction in Martin-Löf type theory (Q1087865) (← links)
- Constructing recursion operators in intuitionistic type theory (Q1094421) (← links)
- Generalized algebraic theories and contextual categories (Q1096716) (← links)
- On the syntax of Martin-Löf's type theories (Q1099173) (← links)
- Algebra of constructions. I. The word problem for partial algebras (Q1107515) (← links)
- The calculus of constructions (Q1108266) (← links)
- About primitive recursive algorithms (Q1176246) (← links)
- Type checking with universes (Q1177937) (← links)
- A bridge between constructive logic and computer programming (Q1179711) (← links)
- Program development in constructive type theory (Q1190474) (← links)
- An intuitionistic theory of types with assumptions of high-arity variables (Q1192333) (← links)
- Constructing type systems over an operational semantics (Q1199709) (← links)
- Representing scope in intuitionistic deductions (Q1274448) (← links)
- From constructivism to computer science (Q1274450) (← links)
- System \(T\), call-by-value and the minimum problem (Q1274979) (← links)
- Process calculus based upon evaluation to committed form (Q1276241) (← links)
- Well-ordering proofs for Martin-Löf type theory (Q1295372) (← links)
- Computational foundations of basic recursive function theory (Q1314348) (← links)
- Realizability interpretation of generalized inductive definitions (Q1331920) (← links)
- Representing inductively defined sets by wellorderings in Martin-Löf's type theory (Q1392287) (← links)
- A constructive approach to state description semantics (Q1414570) (← links)
- Analogical program derivation based on type theory (Q1802072) (← links)
- Extraction and verification of programs by analysis of formal proofs (Q1823656) (← links)
- Towards a computation system based on set theory (Q1825191) (← links)
- The Girard-Reynolds isomorphism (Q1887154) (← links)
- The axioms of constructive geometry (Q1902978) (← links)
- Foundational aspects of multiscale digitization (Q1935768) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- Inverse semigroups with apartness (Q2416389) (← links)
- Axiomatizing geometric constructions (Q2480964) (← links)
- Indexed induction-recursion (Q2577476) (← links)
- One step is enough (Q2679573) (← links)
- (Q3300787) (← links)
- Cartesian cubical computational type theory: Constructive reasoning with paths and equalities (Q5079726) (← links)
- Normalization by Evaluation for Martin-Löf Type Theory with One Universe (Q5262927) (← links)
- The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories – an Intuitionistic Perspective (Q5415629) (← links)
