{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:55:45Z","timestamp":1770274545765,"version":"3.49.0"},"reference-count":35,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,3,27]],"date-time":"2012-03-27T00:00:00Z","timestamp":1332806400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Dependently typed programs contain an excessive amount of static terms which are necessary to please the type checker but irrelevant for computation. To separate static and dynamic code, several static analyses and type systems have been put forward. We consider Pfenning's type theory with irrelevant quantification which is compatible with a type-based notion of equality that respects eta-laws. We extend Pfenning's theory to universes and large eliminations and develop its meta-theory. Subject reduction, normalization and consistency are obtained by a Kripke model over the typed equality judgement. Finally, a type-directed equality algorithm is described whose completeness is proven by a second Kripke model.<\/jats:p>","DOI":"10.2168\/lmcs-8(1:29)2012","type":"journal-article","created":{"date-parts":[[2012,9,6]],"date-time":"2012-09-06T10:03:11Z","timestamp":1346925791000},"source":"Crossref","is-referenced-by-count":23,"title":["On Irrelevance and Algorithmic Equality in Predicative Type Theory"],"prefix":"10.46298","volume":"Volume 8, Issue 1","author":[{"given":"Andreas","family":"Abel","sequence":"first","affiliation":[]},{"given":"Gabriel","family":"Scherer","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,3,27]]},"reference":[{"issue":"4","key":"10.2168\/LMCS-8(1:29)2012_awodeyBauer:propositionsAsTypes","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1093\/logcom\/14.4.447","volume":"14","author":"Steven Awodey and Andrej Bauer","year":"2004","journal-title":"Journal of Logic and Computation"},{"key":"10.2168\/LMCS-8(1:29)2012_abel:nbe09","unstructured":"Andreas Abel. Extensional normalization in the logical framework with proof irrelevant equality. In Olivier Danvy, editor,Workshop on Normalization by Evaluation, affiliated to LiCS 2009, Los Angeles, 15 August 2009, 2009."},{"key":"10.2168\/LMCS-8(1:29)2012_abel:fossacs11","unstructured":"Andreas Abel. Irrelevance in type theory with a heterogeneous equality judgement. In Martin Hofmann, editor,Foundations of Software Science and Computational Structures, 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbr\u00fccken, Germany, March 26 - April 3, 2011. Proceedings}, volume 6604 ofLecture Notes in Computer Science, pages 57-71. Springer-Verlag, 2011."},{"issue":"4","key":"10.2168\/LMCS-8(1:29)2012_abelCoquand:fundinf07","first-page":"345","volume":"77","author":"Andreas Abel and Thierry Coquand","year":"2007","journal-title":"Fundamenta Informaticae TLCA'05 special issue"},{"key":"10.2168\/LMCS-8(1:29)2012_abelCoquandDybjer:lics07","doi-asserted-by":"crossref","unstructured":"Andreas Abel, Thierry Coquand, and Peter Dybjer. Normalization by evaluation for Martin-L\u00f6f Type Theory with typed equality judgements. In22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July 2007, Wroclaw, Poland, Proceedings, pages 3-12. IEEE Computer Society Press, 2007.","DOI":"10.1109\/LICS.2007.33"},{"key":"10.2168\/LMCS-8(1:29)2012_abelCoquandDybjer:mpc08","doi-asserted-by":"crossref","unstructured":"Andreas Abel, Thierry Coquand, and Peter Dybjer. Verifying a semanticbeta eta-conversion test for Martin-L\u00f6f type theory. In Philippe Audebaud and Christine Paulin-Mohring, editors,Mathematics of Program Construction, 9th International Conference, MPC 2008, Marseille, France, July 15-18, 2008. Proceedings, volume 5133 ofLecture Notes in Computer Science, pages 29-56. Springer-Verlag, 2008.","DOI":"10.1007\/978-3-540-70594-9_4"},{"key":"10.2168\/LMCS-8(1:29)2012_abelCoquandPagano:lmcs11","first-page":"4","volume":"2","author":"Andreas Abel, Thierry Coquand, and Migue","year":"2011","journal-title":"Logical Methods in Computer Science"},{"issue":"2","key":"10.2168\/LMCS-8(1:29)2012_adams:jfp06","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1017\/S0956796805005770","volume":"16","author":"Robin Adams","year":"2006","journal-title":"Journal of Functional Programming"},{"key":"10.2168\/LMCS-8(1:29)2012_allen:PhD","unstructured":"Stuart Allen.A Non-Type-Theoretic Semantics for Type-Theoretic Language. PhD thesis, Cornell University, 1987."},{"key":"10.2168\/LMCS-8(1:29)2012_DBLP:conf\/fossacs\/2008","unstructured":"Roberto M. Amadio, editor.Foundations of Software Science and Computational Structures, 11th International Conference, FOSSACS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29 - April 6, 2008. Proceedings, volume 4962 ofLecture Notes in Computer Science. Springer-Verlag, 2008. Lennart Augustsson. Cayenne - a language with dependent types. InProceedings of the third ACM SIGPLAN International Conference on Functional Programming (ICFP '98), Baltimore, Maryland, USA, September 27-29, 1998, volume 34 ofSIGPLAN Notices, pages 239-250. ACM Press, 1999."},{"key":"10.2168\/LMCS-8(1:29)2012_barendregt:lambdacalculus","unstructured":"Henk Barendregt.The Lambda Calculus: Its Syntax and Semantics. North Holland, Amsterdam, 1984."},{"key":"10.2168\/LMCS-8(1:29)2012_barrasBernardo:fossacs08","doi-asserted-by":"crossref","unstructured":"Bruno Barras and Bruno Bernardo. The implicit calculus of constructions as a programming language with dependent types. In Amadio DBLP:conf\/fossacs\/2008, pages 365-379.","DOI":"10.1007\/978-3-540-78499-9_26"},{"key":"10.2168\/LMCS-8(1:29)2012_boveDybjerNorell:tphols09","unstructured":"Ana Bove, Peter Dybjer, and Ulf Norell. A brief overview of Agda - a functional language with dependent types. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors,Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, volume 5674 ofLecture Notes in Computer Science, pages 73-78. Springer-Verlag, 2009."},{"key":"10.2168\/LMCS-8(1:29)2012_constable:nuprl","unstructured":"Robert L. Constable, Stuart F. Allen, Mark Bromley, Rance Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith.Implementing mathematics with the Nuprl proof development system. Prentice Hall, 1986."},{"key":"10.2168\/LMCS-8(1:29)2012_coquand:conversion","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569807.011"},{"key":"10.2168\/LMCS-8(1:29)2012_coquand:type","unstructured":"Thierry Coquand. An algorithm for type-checking dependent types. InMathematics of Program Construction. Selected Papers from the Third International Conference on the Mathematics of Program Construction (July 17-21, 1995, Kloster Irsee, Germany), volume 26 ofScience of Computer Programming, pages 167-177. Elsevier, May 1996."},{"key":"10.2168\/LMCS-8(1:29)2012_goguen:PhD","unstructured":"Healfdene Goguen.A Typed Operational Semantics for Type Theory. PhD thesis, University of Edinburgh, August 1994. Available as LFCS Report ECS-LFCS-94-304."},{"key":"10.2168\/LMCS-8(1:29)2012_goguen:types00","doi-asserted-by":"crossref","unstructured":"Healfdene Goguen. A Kripke-style model for the admissibility of structural rules. In Paul Callaghan, Zhaohui Luo, James McKinna, and Robert Pollack, editors,Types for Proofs and Programs, International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000, Selected Papers, volume 2277 ofLecture Notes in Computer Science, pages 112-124. Springer-Verlag, 2000.","DOI":"10.1007\/3-540-45842-5_8"},{"key":"10.2168\/LMCS-8(1:29)2012_goguen:justifyingAlgorithms","unstructured":"Healfdene Goguen. Justifying algorithms forbeta etaconversion. In Vladimiro Sassone, editor,Foundations of Software Science and Computational Structures, 8th International Conference, FoSSaCS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings, volume 3441 ofLecture Notes in Computer Science, pages 410-424. Springer-Verlag, 2005."},{"issue":"1","key":"10.2168\/LMCS-8(1:29)2012_harperPfenning:equivalenceLF","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1145\/1042038.1042041","volume":"6","author":"Robert Harper and Frank Pfenning","year":"2005","journal-title":"ACM Transactions on Computational Logic"},{"key":"10.2168\/LMCS-8(1:29)2012_inria:coq83","unstructured":"INRIA.The Coq Proof Assistant Reference Manual. INRIA, version 8.3 edition, 2010."},{"key":"10.2168\/LMCS-8(1:29)2012_letouzey:types02","unstructured":"Pierre Letouzey. A new extraction for Coq. In Herman Geuvers and Freek Wiedijk, editors,Types for Proofs and Programs, Second International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, Selected Papers, volume 2646 ofLecture Notes in Computer Science, pages 200-219. Springer-Verlag, 2002."},{"key":"10.2168\/LMCS-8(1:29)2012_miquel:lics00","doi-asserted-by":"crossref","unstructured":"Alexandre Miquel. A model for impredicative type systems, universes, intersection types and subtyping. In15th IEEE Symposium on Logic in Computer Science (LICS 2000), 26-29 June 2000, Santa Barbara, California, USA, Proceedings, pages 18-29, 2000.","DOI":"10.1109\/LICS.2000.855752"},{"key":"10.2168\/LMCS-8(1:29)2012_miquel:tlca01","doi-asserted-by":"crossref","unstructured":"Alexandre Miquel. The implicit calculus of constructions. In Samson Abramsky, editor,Typed Lambda Calculi and Applications, 5th International Conference, TLCA 2001, Krakow, Poland, May 2-5, 2001, Proceedings, volume 2044 ofLecture Notes in Computer Science, pages 344-359. Springer-Verlag, 2001.","DOI":"10.1007\/3-540-45413-6_27"},{"key":"10.2168\/LMCS-8(1:29)2012_miquel:PhD","unstructured":"Alexandre Miquel.Le Calcul des Constructions implicite: syntaxe et s\u00e9mantique. PhD thesis, Universit\u00e9 Paris 7, December 2001."},{"key":"10.2168\/LMCS-8(1:29)2012_mishraLinger:PhD","unstructured":"Richard Nathan Mishra-Linger.Irrelevance, Polymorphism, and Erasure in Type Theory. PhD thesis, Portland State University, 2008."},{"key":"10.2168\/LMCS-8(1:29)2012_mishraLingerSheard:fossacs08","doi-asserted-by":"crossref","unstructured":"Nathan Mishra-Linger and Tim Sheard. Erasure and polymorphism in pure type systems. In Amadio DBLP:conf\/fossacs\/2008, pages 350-364.","DOI":"10.1007\/978-3-540-78499-9_25"},{"issue":"1","key":"10.2168\/LMCS-8(1:29)2012_mcBrideMcKinna:view","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1017\/S0956796803004829","volume":"14","author":"Conor McBride and James McKinna","year":"2004","journal-title":"Journal of Functional Programming"},{"key":"10.2168\/LMCS-8(1:29)2012_pfenning:intextirr","doi-asserted-by":"crossref","unstructured":"Frank Pfenning. Intensionality, extensionality, and proof irrelevance in modal type theory. In16th IEEE Symposium on Logic in Computer Science (LICS 2001), 16-19 June 2001, Boston University, USA, Proceedings. IEEE Computer Society Press, 2001.","DOI":"10.1109\/LICS.2001.932499"},{"issue":"5\/6","key":"10.2168\/LMCS-8(1:29)2012_paulinWerner:jsc93","first-page":"607","volume":"15","author":"Christine Paulin-Mohring and Benjamin We","year":"1993","journal-title":"Journal of Symbolic Computation"},{"key":"10.2168\/LMCS-8(1:29)2012_reed:thesis","unstructured":"Jason Reed. Proof irrelevance and strict definitions in a logical framework, 2002. Senior Thesis, published as Carnegie-Mellon University technical report CMU-CS-02-153."},{"key":"10.2168\/LMCS-8(1:29)2012_reed:tphols03","doi-asserted-by":"crossref","unstructured":"Jason Reed. Extending higher-order unification to support proof irrelevance. In David A. Basin and Burkhart Wolff, editors,Theorem Proving in Higher Order Logics, 16th International Conference, TPHOLs 2003, Rom, Italy, September 8-12, 2003, Proceedings, volume 2758 ofLecture Notes in Computer Science, pages 238-252. Springer-Verlag, 2003.","DOI":"10.1007\/10930755_16"},{"key":"10.2168\/LMCS-8(1:29)2012_schuermannSarnat:lics08","doi-asserted-by":"crossref","unstructured":"Carsten Sch\u00fcrmann and Jeffrey Sarnat. Structural logical relations. In Frank Pfenning, editor,Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA, pages 69-80. IEEE Computer Society Press, 2008.","DOI":"10.1109\/LICS.2008.44"},{"key":"10.2168\/LMCS-8(1:29)2012_vanderwaartCrary:lfm02","unstructured":"Joseph C. Vanderwaart and Karl Crary. A simplified account of the metatheory of Linear LF. InThird International Workshop on Logical Frameworks and Metalanguages (LFM 2002), FLoC'02 affiliated workshop, Copenhagen, Denmark, 2002. An extended version appeared as CMU Technical Report CMU-CS-01-154."},{"key":"10.2168\/LMCS-8(1:29)2012_werner:lmcs08","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-4(3:13)2008"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1045\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1045\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T23:10:18Z","timestamp":1744067418000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1045"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,3,27]]},"references-count":35,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(1:29)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1203.4716","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1203.4716","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,3,27]]},"article-number":"1045"}}