scientific article; zbMATH DE number 226803
From MaRDI portal
Publication:5286647
Metamathematics of constructive systems (03F50) Theories (e.g., algebraic theories), structure, and semantics (18C10) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Semantics in the theory of computing (68Q55)
Recommendations
- La théorie intuitionniste des types : sémantique des preuves et théorie des constructions
- The completeness of typing for context-semantics
- scientific article; zbMATH DE number 4027461
- scientific article; zbMATH DE number 5872251
- scientific article; zbMATH DE number 895270
- Algebra and Coalgebra in Computer Science
- Completeness theorems for first-order logic analysed in constructive type theory
- Completeness theorems for first-order logic analysed in constructive type theory
- A proof-theoretic characterization of independence in type theory
- On the syntax of Martin-Löf's type theories
Cited in
(69)- A minimalist two-level foundation for constructive mathematics
- Independence of the induction principle and the axiom of choice in the pure calculus of constructions
- On the structure of paradoxes
- Typed operational semantics for higher-order subtyping.
- The algebra of partial equivalence relations
- The homotopy theory of type theories
- On completeness and cocompleteness in and around small categories
- Coreflections in algebraic quantum logic
- The simplicial model of univalent foundations (after Voevodsky)
- Semantical analysis of contextual types
- Proof-theoretic semantics for classical mathematics
- Containers: Constructing strictly positive types
- Nominal lambda calculus: an internal language for FM-Cartesian closed categories
- Observability in the univalent universe
- C-system of a module over a \(Jf\)-relative monad
- Type theory should eat itself
- A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory
- Dependent types and fibred computational effects
- Joyal's arithmetic universes via type theory
- Pure type system conversion is always typable
- The intrinsic topology of Martin-Löf universes
- Products of families of types and (Pi,lambda)-structures on C-systems
- C-systems defined by universe categories: presheaves
- The (Pi,lambda)-structures on the C-systems defined by universe categories
- scientific article; zbMATH DE number 2185666 (Why is no real title available?)
- A homotopy-theoretic model of function extensionality in the effective topos
- Kripke Semantics for Martin-Löf’s Extensional Type Theory
- scientific article; zbMATH DE number 4027461 (Why is no real title available?)
- Cubical type theory: a constructive interpretation of the univalence axiom
- Reflective semantics of constructive type theory
- Type theoretic semantics for SemNet
- Brouwer's fixed-point theorem in real-cohesive homotopy type theory
- Collapsing partial combinatory algebras
- A simple model construction for the calculus of constructions
- scientific article; zbMATH DE number 2154393 (Why is no real title available?)
- Semantics of higher inductive types
- Categories with families: unityped, simply typed, and dependently typed
- Extensional equality preservation and verified generic programming
- The Interpretation Lifting Theorem for C-Systems
- Canonicity and homotopy canonicity for cubical type theory
- Doctrines, modalities and comonads
- Martin Hofmann’s contributions to type theory: Groupoids and univalence
- On generalized algebraic theories and categories with families
- Homotopy canonicity for cubical type theory
- Cubical syntax for reflection-free extensional equality
- Signatures and induction principles for higher inductive-inductive types
- Type theory and homotopy
- A dependent type theory with abstractable names
- The axiom of choice in cartesian bicategories
- Finitary type theories with and without contexts
- The metatheory of UTT
- Models of HoTT and the Constructive View of Theories
- For Finitary Induction-Induction, Induction is Enough
- Proving strong normalization of CC by modifying realizability semantics
- Elimination of extensionality in Martin-Löf type theory
- Martin-Löf identity types in C-systems
- On the ∞$\infty$‐topos semantics of homotopy type theory
- An intuitionistic set-theoretical model of fully dependent CC
- Classical predicative logic-enriched type theories
- Synthetic domain theory in type theory: another logic of computable functions
- Toward a geometry for syntax
- Relating homotopy equivalences to conservativity in dependent type theories with computation axioms
- Extracting efficient exact real number computation from proofs in constructive type theory
- Globular weak -categories as models of a type theory
- Algebraic presentations of type dependency
- The category of iterative sets in homotopy type theory and univalent foundations
- Realizability models refuting Ishihara's boundedness principle
- A 2-categorical approach to the semantics of dependent type theory with computation axioms
- The proof monad
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5286647)
