An Intuitionistic Set-theoretical Model of the Extended Calculus of Constructions
Logic in Computer Science
2015-02-17 v3
Abstract
Werner's set-theoretical model is one of the most intuitive models of ECC. It combines a functional view of predicative universes with a collapsed view of the impredicative sort Prop. However this model of Prop is so coarse that the principle of excluded middle holds. In this paper, we interpret Prop into a topological space (a special case of Heyting algebra) to make it more intuitionistic without sacrificing simplicity. We prove soundness and show some applications of our model.
Keywords
Cite
@article{arxiv.1412.2235,
title = {An Intuitionistic Set-theoretical Model of the Extended Calculus of Constructions},
author = {Masahiro Sato},
journal= {arXiv preprint arXiv:1412.2235},
year = {2015}
}