scientific article
From MaRDI portal
Publication:2871881
zbMath1278.03056MaRDI QIDQ2871881
Peter Dybjer, Alexandre Buisse
Publication date: 10 January 2014
Full work available at URL: http://www.sciencedirect.com/science/article/pii/S1571066108000431?np=y
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
constructive type theorycategorical logicdependent typesproof assistantscategories with familiesinternal type theory
Logic in computer science (03B70) Categorical logic, topoi (03G30) Second- and higher-order arithmetic and fragments (03F35)
Related Items (2)
The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories – an Intuitionistic Perspective ⋮ Type Theory Should Eat Itself
Uses Software
This page was built for publication:
