The following pages link to (Q3328540):
Displaying 41 items.
- Intuitionistic completeness of first-order logic (Q392280) (← links)
- Using formal methods with SysML in aerospace design and engineering (Q434438) (← links)
- Coalgebras in functional programming and type theory (Q639643) (← links)
- Applause: An implementation of the Collins-Michalski theory of plausible reasoning (Q751307) (← links)
- Insight in discrete geometry and computational content of a discrete model of the continuum (Q834257) (← links)
- Constructive system for automatic program synthesis (Q912589) (← links)
- A computer-verified monadic functional implementation of the integral (Q987984) (← links)
- A small complete category (Q1112159) (← 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)
- Between constructive mathematics and PROLOG (Q1173742) (← links)
- Partial inductive definitions (Q1177153) (← links)
- Static semantics, types, and binding time analysis (Q1179698) (← links)
- Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\) (Q1295369) (← links)
- IMPS: An interactive mathematical proof system (Q1319391) (← links)
- Induction-recursion and initial algebras. (Q1412830) (← links)
- Some points in formal topology. (Q1427787) (← links)
- Proof-search in type-theoretic languages: An introduction (Q1575935) (← links)
- The origins of structural operational semantics (Q1878710) (← links)
- Middle-out reasoning for synthesis and induction (Q1915136) (← links)
- A meaning explanation for HoTT (Q2054122) (← links)
- Predicativity and constructive mathematics (Q2080590) (← links)
- Formally computing with the non-computable (Q2117773) (← links)
- A characterisation of elementary fibrations (Q2131276) (← links)
- Towards a directed homotopy type theory (Q2133175) (← links)
- A type-theoretic approach to program development (Q2277827) (← links)
- The justification of identity elimination in Martin-Löf's type theory (Q2288279) (← links)
- An adequacy theorem for dependent type theory (Q2311883) (← links)
- From signatures to monads in \textsf{UniMath} (Q2319990) (← links)
- Connectionist computations of intuitionistic reasoning (Q2503271) (← links)
- Constructive algebraic integration theory (Q2575777) (← links)
- A Classical Realizability Model for a Semantical Value Restriction (Q2802494) (← links)
- Homotopy type theory and Voevodsky’s univalent foundations (Q2933829) (← links)
- Turing-Completeness Totally Free (Q2941179) (← links)
- Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language (Q2947456) (← links)
- A Proposal for Broad Spectrum Proof Certificates (Q3100201) (← links)
- From Mathesis Universalis to Provability, Computability, and Constructivity (Q3305633) (← links)
- An introduction to univalent foundations for mathematicians (Q4684362) (← links)
- ETA-RULES IN MARTIN-LÖF TYPE THEORY (Q5240810) (← links)
- Finitary type theories with and without contexts (Q6053849) (← links)
- A Survey of the Proof-Theoretic Foundations of Logic Programming (Q6063891) (← links)
- Martin-Löf identity types in C-systems (Q6139425) (← links)
