Propositions as [Types]

DOI10.1093/LOGCOM/14.4.447MaRDI QIDQ4823804zbMATH OpenOpenAlexWikidataFDO

Authors Andrej Bauer, Steve Awodey

Publication date 28 October 2004

Published in Journal Of Logic And Computation (Search for Journal in Brave)

Full work available at URL https://semanticscholar.org/paper/0903e5c7842fbd261d1e2364ff1ba7b636204052

zbMATH Keywords

bracket typescategory theoryintuitionistic logicmodal logicregular categoriestype theory

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Categorical logic, topoi (03G30) Categorical semantics of formal languages (18C50)

Recommendations

• Modular correspondence between dependent type theories and categories including pretopoi and topoi
• scientific article; zbMATH DE number 2079044
• scientific article; zbMATH DE number 1531359
• Dependence and independence results for (impredicative) calculi of dependent types
• Functional completeness of the free locally Cartesian closed category and interpretations of Martin-Löf's theory of dependent types

Cited in

(30)

• Fibrational modal type theory
• Curry-Howard-Lambek correspondence for intuitionistic belief
• Hybridizing a logical framework
• Notions of anonymous existence in Martin-Löf type theory
• Proof-carrying code in a session-typed process calculus
• Mathesis Universalis and Homotopy Type Theory
• A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance
• Refinement Types as Proof Irrelevance
• Foundations of dependent interoperability
• A SYNTACTIC CHARACTERIZATION OF MORITA EQUIVALENCE
• Propositions
• An introduction to univalent foundations for mathematicians
• On Church’s thesis in cubical assemblies
• Cubical syntax for reflection-free extensional equality
• Cubical assemblies, a univalent and impredicative universe and a failure of propositional resizing
• A cubical language for Bishop sets
• Dual-context calculi for modal logic
• Modalities in homotopy type theory
• Modal dependent type theory and dependent right adjoints
• The generalised type-theoretic interpretation of constructive set theory
• Sets in homotopy type theory
• Lifschitz realizability as a topological construction
• From type theory to setoids and back
• A class of higher inductive types in Zermelo‐Fraenkel set theory
• Topological quantum gates in homotopy type theory
• Kripke-Joyal forcing for type theory and uniform fibrations
• Apartness relations between propositions
• A denotationally-based program logic for higher-order store
• Hyperintensions as computations
• Separating path and identity types in presheaf models of univalent type theory

This page was built for publication: Propositions as [Types]

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4823804)