@inbook{f8ee7821f94a49f1b479c4a45dccdb9a,
title = "Collection principles in dependent type theory",
abstract = "We introduce logic-enriched intuitionistic type theories, that extend intuitionistic dependent type theories with primitive judgements to express logic. By adding type theoretic rules that correspond to the collection axiom schemes of the constructive set theory CZF we obtain a generalisation of the type theoretic interpretation of CZF. Suitable logic-enriched type theories allow also the study of reinterpretations of logic. We end the paper with an application to the double-negation interpretation.",
keywords = "inference rule, type theory, Intuitionistic Logic, double negation, induction rule",
author = "Peter Aczel and Nicola Gambino",
year = "2002",
month = feb,
day = "14",
doi = "10.1007/3-540-45842-5_1",
language = "English",
isbn = "9783540432876",
series = "Lecture Notes in Computer Science",
publisher = "Springer Berlin",
pages = "1--23",
editor = "Paul Callaghan and Zhaohui Luo and James McKinna and Robert Pollack",
booktitle = "Types for proofs and programs",
address = "Germany",
}