Proof-irrelevant model of CC with predicative induction and judgmental equality
From MaRDI portal
Publication:3224695
DOI10.2168/LMCS-7(4:5)2011zbMath1237.03008arXiv1111.0123OpenAlexW1971086784MaRDI QIDQ3224695
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/1111.0123
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (3)
Wave equation numerical resolution: a comprehensive mechanized proof of a C program ⋮ An intuitionistic set-theoretical model of fully dependent CC ⋮ Cumulative Inductive Types in Coq
Uses Software
This page was built for publication: Proof-irrelevant model of CC with predicative induction and judgmental equality
