The following pages link to (Q3328540):
Displaying 50 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)
- Building Mathematics-Based Software Systems to Advance Science and Create Knowledge (Q3644710) (← links)
- (Q4029339) (← links)
- An introduction to univalent foundations for mathematicians (Q4684362) (← links)
- THE CONCEPT<i>HORSE</i>IS A CONCEPT (Q4961743) (← links)
- Categories with Families: Unityped, Simply Typed, and Dependently Typed (Q5014596) (← links)
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs (Q5019018) (← links)
- (Q5028425) (← links)
- Applications of type theory (Q5044747) (← links)
- Cubical methods in homotopy type theory and univalent foundations (Q5055493) (← links)
- Type theory as a foundation for computer science (Q5096219) (← links)
- Some normalization properties of martin-löf's type theory, and applications (Q5096234) (← links)
- A generic algebra for data collections based on constructive logic (Q5096406) (← links)
- POPLMark reloaded: Mechanizing proofs by logical relations (Q5110924) (← links)
- W-types in setoids (Q5155691) (← links)
