@inbook{2b3cd9fe67684fe0b6f39684c3b93382,
title = "The not so simple proof-irrelevant model of CC",
abstract = "It is well-known that the Calculus of Constructions (CC) bears a simple set-theoretical model in which proof-terms are mapped onto a single object - a property which is known as proof-irrelevance. In this paper, we show that when going into the (generally omitted) technical details, this naive model raises several unexpected difficulties related to the interpretation of the impredicative level, especially for the soundness property which is surprisingly difficult to be given a correct proof in this simple framework. We propose a way to tackle these difficulties, thus giving a (more) detailed elementary consistency proof of CC without going back to a translation to Fω. We also discuss some possible alternatives and possible extensions of our construction.",
author = "Alexandre Miquel and Benjamin Werner",
year = "2003",
month = jan,
day = "1",
doi = "10.1007/3-540-39185-1\_14",
language = "English",
isbn = "354014031X",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "240--258",
editor = "Herman Geuvers and Freek Wiedijk",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
}