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

category theoryintuitionistic logicmodal logictype theoryregular categoriesbracket types

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

(27)

• scientific article; zbMATH DE number 7243672 (Why is no real title available?)
• A SYNTACTIC CHARACTERIZATION OF MORITA EQUIVALENCE
• Fibrational modal type theory
• Topological quantum gates in homotopy type theory
• A class of higher inductive types in Zermelo‐Fraenkel set theory
• Kripke-Joyal forcing for type theory and uniform fibrations
• Lifschitz realizability as a topological construction
• Mathesis Universalis and Homotopy Type Theory
• From type theory to setoids and back
• Refinement Types as Proof Irrelevance
• Hybridizing a logical framework
• Sets in homotopy type theory
• On Church’s thesis in cubical assemblies
• scientific article; zbMATH DE number 7561492 (Why is no real title available?)
• The generalised type-theoretic interpretation of constructive set theory
• Curry-Howard-Lambek correspondence for intuitionistic belief
• Propositions
• scientific article; zbMATH DE number 7559297 (Why is no real title available?)
• Apartness relations between propositions
• Modalities in homotopy type theory
• Modal dependent type theory and dependent right adjoints
• A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance
• scientific article; zbMATH DE number 7566056 (Why is no real title available?)
• Notions of anonymous existence in Martin-Löf type theory
• Foundations of dependent interoperability
• Proof-carrying code in a session-typed process calculus
• An introduction to univalent foundations for mathematicians

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)