Propositions as [Types]

DOI10.1093/LOGCOM/14.4.447zbMATH Open1050.03016OpenAlexW2121730419WikidataQ115902571 ScholiaQ115902571MaRDI QIDQ4823804FDOQ4823804

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

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

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)

Cited In (27)

• Title not available (Why is that?)
• A SYNTACTIC CHARACTERIZATION OF MORITA EQUIVALENCE
• Topological quantum gates in homotopy type theory
• Fibrational modal type theory
• Kripke-Joyal forcing for type theory and uniform fibrations
• A class of higher inductive types in Zermelo‐Fraenkel set theory
• 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
• Title not available (Why is that?)
• The generalised type-theoretic interpretation of constructive set theory
• Curry-Howard-Lambek correspondence for intuitionistic belief
• Propositions
• Apartness relations between propositions
• Title not available (Why is that?)
• 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
• Title not available (Why is that?)
• Foundations of dependent interoperability
• Notions of anonymous existence in Martin-Löf type theory
• 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)