Kripke Semantics for Martin-L\"of's Extensional Type Theory
From MaRDI portal
Publication:3224684
DOI10.2168/LMCS-7(3:18)2011zbMath1237.03007arXiv1109.1702MaRDI QIDQ3224684
Publication date: 2 April 2012
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1109.1702
Categorical logic, topoi (03G30) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15)
Related Items
Kripke semantics for higher-order type theory applied to constraint logic programming languages, Kripke Semantics for Martin-Löf’s Extensional Type Theory
Uses Software