Propositions as [Types]

DOI10.1093/logcom/14.4.447zbMath1050.03016OpenAlexW2121730419WikidataQ115902571 ScholiaQ115902571MaRDI QIDQ4823804

Andrej Bauer, Steven 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

modal logiccategory theoryintuitionistic 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)

Related Items (23)

Modalities in homotopy type theory ⋮ From type theory to setoids and back ⋮ Unnamed Item ⋮ On Church’s thesis in cubical assemblies ⋮ Foundations of dependent interoperability ⋮ A class of higher inductive types in Zermelo‐Fraenkel set theory ⋮ A SYNTACTIC CHARACTERIZATION OF MORITA EQUIVALENCE ⋮ Mathesis Universalis and Homotopy Type Theory ⋮ Fibrational modal type theory ⋮ Sets in homotopy type theory ⋮ Unnamed Item ⋮ Unnamed Item ⋮ An introduction to univalent foundations for mathematicians ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Modal dependent type theory and dependent right adjoints ⋮ A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance ⋮ Refinement Types as Proof Irrelevance ⋮ The generalised type-theoretic interpretation of constructive set theory ⋮ Curry-Howard-Lambek correspondence for intuitionistic belief ⋮ Proof-Carrying Code in a Session-Typed Process Calculus ⋮ LIFSCHITZ REALIZABILITY AS A TOPOLOGICAL CONSTRUCTION ⋮ Hybridizing a Logical Framework

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