https://github.com/AndrasKovacs/universes
Tip revision: dfb2127865dda7ab2db1a29ea1a2d5ac3d60f4b5 authored by AndrasKovacs on 29 October 2021, 18:43:22 UTC
fixes
fixes
Tip revision: dfb2127
references.bib
@INPROCEEDINGS{abadi96explicitsubstitutions,
author = {Martin Abadi and Luca Cardelli and Pierre-Louis Curien and Jean-Jacques L{\'e}vy},
title = {Explicit substitutions},
year = {1996},
booktitle = {Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, California},
publisher = {ACM}
}
@phdthesis{cartmellthesis,
author = {John Cartmell},
title = {Generalised algebraic theories and contextual categories},
school = {Oxford University},
year = {1978}}
@phdthesis{abbottthesis,
author = {Michael Gordon Abbott},
title = {Categories of containers},
school = {University of Leicester},
year = {2003}}
@Article{abbot05containers,
author = {Michael Abbott and Thorsten Altenkirch and Neil Ghani},
title = {Containers --- Constructing Strictly Positive Types},
journal = {Theoretical Computer Science},
year = {2005},
volume = {342},
pages = {3--27},
month = {September},
note = {Applied Semantics: Selected Topics},
}
@Misc{altenkirch92,
Author = {Thorsten Altenkirch},
Title = {An open question concerning inductive equality. E-mail message to the Edinburgh LEGO club},
Year = 1992}
@Article{altenkirch09bigstep,
title={{Big-step normalisation}},
author={Thorsten Altenkirch and James Chapman},
journal={Journal of Functional Programming},
volume={19},
number={3-4},
pages={311--333},
year={2009},
publisher={Cambridge University Press}
}
@INPROCEEDINGS{altenkirch07observational,
author = {Thorsten Altenkirch and Conor Mcbride and Wouter Swierstra},
title = {Observational Equality, Now!},
booktitle = {PLPV '07: Proceedings of the 2007 workshop on Programming languages meets program verification},
publisher = {ACM},
year = {2007},
pages = {57--58}}
@INPROCEEDINGS{altenkirch11ii,
author = {Altenkirch, Thorsten and Morris, Peter and
Nordvall Forsberg, Fredrik and Setzer, Anton},
title = {A categorical semantics for inductive-inductive definitions},
booktitle = {CALCO},
editor = {Corradini, Andrea and Klin, Bartek},
series = {Lecture Notes in Computer Science},
year = {2011}
}
@article{awodey07,
author = {Awodey, Steve and Warren, Michael A.},
day = {3},
doi = {10.1017/s0305004108001783},
eprint = {0709.0248},
keywords = {axiom-k, coquand-bologna, homotopy-theory, inductive-families},
month = sep,
posted-at = {2010-03-11 16:56:23},
priority = {2},
title = {{Homotopy theoretic models of identity types}},
url = {http://dx.doi.org/10.1017/s0305004108001783},
year = {2007}
}
@PHDTHESIS{forsberg-phd,
author = {Nordvall Forsberg, Fredrik},
title = {Inductive-inductive definitions},
school = {Swansea University},
year = {2013}}
@book{awodey2010category,
title={Category Theory},
author={Awodey, S.},
isbn={9780199587360},
lccn={2010483708},
series={Oxford Logic Guides},
url={http://books.google.co.uk/books?id=-MCJ6x2lC7oC},
year={2010},
publisher={OUP Oxford}
}
@article{barendregt00cut,
added-at = {2011-06-10T00:00:00.000+0200},
author = {Barendregt, Henk and Ghilezan, Silvia},
biburl = {http://www.bibsonomy.org/bibtex/25ebc54469e6bfc6af38a65eae29b2f35/dblp},
ee = {http://journals.cambridge.org/action/displayAbstract?aid=44279},
interhash = {45810901ce960d8e50ae17aaefe8d29d},
intrahash = {5ebc54469e6bfc6af38a65eae29b2f35},
journal = {J. Funct. Program.},
keywords = {dblp},
number = 1,
pages = {121-134},
timestamp = {2011-06-10T00:00:00.000+0200},
title = {Lambda terms for natural deduction, sequent calculus and cut elimination.},
url = {http://dblp.uni-trier.de/db/journals/jfp/jfp10.html#BarendregtG00},
volume = 10,
year = 2000
}
@Inproceedings{berger91nbe,
Author = "Ulrich Berger and Helmut Schwichtenberg",
Title = "An inverse of the evaluation functional for
typed $\lambda$--calculus",
Booktitle = "Proceedings of the Sixth Annual IEEE
Symposium on Logic in Computer Science",
Editor = "R. Vemuri",
Pages = "203--211",
Publisher = "IEEE Computer Society Press, Los Alamitos",
Year = 1991}
@Article{bernardy12parametricity,
author = {Jean-Philippe Bernardy and Patrik Jansson and Ross Paterson},
title = {Proofs for Free --- Parametricity for Dependent Types},
journal = {Journal of Functional Programming},
doi = {10.1017/S0956796812000056},
year = {2012},
volume = {22},
number = {02},
pages = {107--152}
},
@inproceedings{cubical,
title={A model of type theory in cubical sets},
author={Bezem, Marc and Coquand, Thierry and Huber, Simon},
booktitle={19th International Conference on Types for Proofs and Programs (TYPES 2013)},
volume={26},
pages={107--128},
year={2014}
}
@INPROCEEDINGS{bovecapretta00,
author = {Ana Bove and Venanzio Capretta},
title = {Nested General Recursion and Partiality in Type Theory},
booktitle = {Theorem Proving in Higher Order Logics: 14th International Conference, TPHOLs 2001, volume 2152 of Lecture Notes in Computer Science},
year = {2000},
pages = {121--135},
publisher = {Springer-Verlag}
}
@article{brady13idris,
author = {Edwin Brady},
title = {Idris, a general-purpose dependently typed programming language:
Design and implementation},
journal = {J. Funct. Program.},
volume = {23},
number = {5},
year = {2013},
pages = {552-593},
ee = {http://dx.doi.org/10.1017/S095679681300018X},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{capretta11coalgebras,
author = {Venanzio Capretta},
title = {Coalgebras in functional programming and type theory},
journal = {Theoretical Computer Science},
volume = {412},
number = {38},
pages = {5006--5024},
year = {2011},
note = {CMCS Tenth Anniversary Meeting},
issn = {0304-3975},
doi = {10.1016/j.tcs.2011.04.024},
url = {http://www.sciencedirect.com/science/article/pii/S0304397511003227}
}
@inproceedings{capriotti13applicative,
author = {Paolo Capriotti and
Ambrus Kaposi},
title = {Free Applicative Functors},
booktitle = {Proceedings 5th Workshop on Mathematically Structured Functional Programming,
{MSFP} 2014, Grenoble, France, 12 April 2014.},
year = {2014},
pages = {2--30},
url = {http://dx.doi.org/10.4204/EPTCS.153.2},
doi = {10.4204/EPTCS.153.2},
timestamp = {Thu, 18 Sep 2014 18:35:34 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/CapriottiK14},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{gat,
title={Generalised algebraic theories and contextual categories},
author={Cartmell, John},
journal={Annals of Pure and Applied Logic},
volume={32},
pages={209--243},
year={1986},
publisher={Elsevier}
}
@article{chapman09eatitself,
author = {James Chapman},
title = {Type Theory Should Eat Itself},
journal = {Electronic Notes in Theoretical Computer Science},
issue_date = {January, 2009},
volume = {228},
month = jan,
year = {2009},
issn = {1571-0661},
pages = {21--36},
numpages = {16},
url = {http://dx.doi.org/10.1016/j.entcs.2008.12.114},
doi = {10.1016/j.entcs.2008.12.114},
acmid = {1496402},
publisher = {Elsevier Science Publishers B. V.},
address = {Amsterdam, The Netherlands, The Netherlands},
keywords = {Agda, big-step normalisation, explicit substitutions, type theory, typed syntax}}
@ARTICLE{coquand91treeparadox,
author = {Thierry Coquand},
title = {The paradox of trees in Type Theory},
journal = {BIT},
year = {1991},
volume = {32}
}
@Unpublished{coquand12semi,
author = {Bruno Barras and Thierry Coquand and Simon Huber},
title = {A Generalization of {T}akeuti-{G}andy Interpretation},
note = {\url{http://uf-ias-2012.wikispaces.com/file/view/semi.pdf}},
year = 2013}
@Unpublished{coquand12simplicial,
author = {Thierry Coquand and Simon Huber},
title = {Simplicial sets model of type theory},
note = {\url{http://www.cse.chalmers.se/~coquand/decuniv.pdf}},
year = 2013}
@Unpublished{coquand12setoid,
author = {Thierry Coquand},
title = {About the setoid model},
note = {\url{http://www.cse.chalmers.se/~coquand/setoid.pdf}},
year = 2013}
@Unpublished{coquand12wmltt,
author = {Thierry Coquand},
title = {Weak Type Theory},
note = {\url{http://www.cse.chalmers.se/~coquand/wmltt.pdf}},
year = 2012}
@inproceedings{danielsson06fastandloose,
added-at = {2006-02-21T00:00:00.000+0100},
author = {Danielsson, Nils Anders and Hughes, John and Jansson, Patrik and Gibbons, Jeremy},
biburl = {http://www.bibsonomy.org/bibtex/23a1531702ce02f17fdabbf7dfb597c4e/dblp},
booktitle = {POPL},
editor = {Morrisett, J. Gregory and Jones, Simon L. Peyton},
ee = {http://doi.acm.org/10.1145/1111037.1111056},
isbn = {1-59593-027-2},
keywords = {dblp},
pages = {206-217},
publisher = {ACM},
timestamp = {2006-02-21T00:00:00.000+0100},
title = {Fast and loose reasoning is morally correct.},
url = {http://dblp.uni-trier.de/db/conf/popl/popl2006.html#DanielssonHJG06},
year = 2006
}
@inproceedings{Dybjer96internaltype,
author = {Peter Dybjer},
editor = {Stefano Berardi and
Mario Coppo},
title = {Internal Type Theory},
booktitle = {Types for Proofs and Programs, International Workshop TYPES'95, Torino,
Italy, June 5-8, 1995, Selected Papers},
series = {Lecture Notes in Computer Science},
volume = {1158},
pages = {120--134},
publisher = {Springer},
year = {1995},
url = {https://doi.org/10.1007/3-540-61780-9\_66},
doi = {10.1007/3-540-61780-9\_66},
timestamp = {Tue, 14 May 2019 10:00:42 +0200},
biburl = {https://dblp.org/rec/conf/types/Dybjer95.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@ARTICLE{dybjer00ir,
author = {Peter Dybjer},
title = {A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory},
journal = {Journal of Symbolic Logic},
year = {2000},
volume = {65},
pages = {525--549}
}
@article{eilenberg:category45,
author = {Eilenberg, Samuel and MacLane, Saunders},
citeulike-article-id = {594561},
journal = {Trans. Amer. Math. Soc.},
keywords = {bibtex-import},
pages = {231--294},
posted-at = {2006-04-21 15:58:46},
priority = {2},
title = {{General theory of natural equivalences}},
volume = {58},
year = {1945}
}
@article{girard71buraliforti,
author = {Girard, J. Y.},
booktitle = {{Proceedings of the second Scandinavian Logic symposium}},
keywords = {imported},
organization = {{North-Holland}},
pages = {63-92},
title = {{Une extension de l{'}interpretation de Godel a l{'}analyse, et son application a l{'}elimination des coupures dans l{'}analyse et la theorie des types}},
volume = {{63}},
year = {{1971}}
}
@article{girard86systemf,
added-at = {2011-09-07T00:00:00.000+0200},
author = {Girard, Jean-Yves},
biburl = {http://www.bibsonomy.org/bibtex/258a0e394090fad8c6c84d1483cbcaa7b/dblp},
ee = {http://dx.doi.org/10.1016/0304-3975(86)90044-7},
interhash = {e7ef71e9f15b5878f9a89e504b6732c2},
intrahash = {58a0e394090fad8c6c84d1483cbcaa7b},
journal = {Theor. Comput. Sci.},
keywords = {dblp},
number = 2,
pages = {159-192},
timestamp = {2011-09-07T00:00:00.000+0200},
title = {The System {F} of Variable Types, Fifteen Years Later.},
url = {http://dblp.uni-trier.de/db/journals/tcs/tcs45.html#Girard86},
volume = 45,
year = 1986
}
@ARTICLE{girard87linear,
AUTHOR = "Jean-Yves Girard",
TITLE = "Linear Logic",
JOURNAL = "Theoretical Computer Science",
PAGES = {1-102},
YEAR = {1987},
}
@book{girard89proofsandtypes,
author = {Girard, Jean-Yves and Taylor, Paul and Lafont, Yves},
title = {Proofs and types},
year = {1989},
isbn = {0-521-37181-3},
publisher = {Cambridge University Press},
address = {New York, NY, USA},
}
@INPROCEEDINGS{goguen06eliminatingdependent,
author = {Healfdene Goguen and Conor Mcbride and James Mckinna},
title = {Eliminating dependent pattern matching},
booktitle = {of Lecture Notes in Computer Science},
year = {2006},
pages = {521--540},
publisher = {Springer}
}
@unpublished{gonthier05,
author = {Gonthier, Georges},
citeulike-article-id = {7631006},
citeulike-linkout-0 = {http://research.microsoft.com/\~{}gonthier/4colproof.pdf},
keywords = {coq, master-project, theorem-proving, verification},
posted-at = {2010-08-13 13:39:53},
priority = {0},
title = {{A computer-checked proof of the Four Colour Theorem}},
url = {http://research.microsoft.com/\~{}gonthier/4colproof.pdf},
year = {2005}
}
@inproceedings{beluga,
author = {Pientka, Brigitte and Dunfield, Joshua},
title = {Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)},
booktitle = {Proceedings of the 5th International Conference on Automated Reasoning},
series = {IJCAR'10},
year = {2010},
isbn = {3-642-14202-8, 978-3-642-14202-4},
location = {Edinburgh, UK},
pages = {15--21},
numpages = {7},
acmid = {2176672},
publisher = {Springer-Verlag},
address = {Berlin, Heidelberg},
}
@article{Harper93lf,
author = {Harper, Robert and Honsell, Furio and Plotkin, Gordon},
title = {A framework for defining logics},
journal = {J. ACM},
issue_date = {Jan. 1993},
volume = {40},
number = {1},
month = jan,
year = {1993},
issn = {0004-5411},
pages = {143--184},
numpages = {42},
url = {http://doi.acm.org/10.1145/138027.138060},
doi = {10.1145/138027.138060},
acmid = {138060},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {formal systems, interactive theorem proving, proof checking, typed lambda calculus},
}
@book{hofmann95extensional,
title={Extensional concepts in intensional type theory},
author={Martin Hofmann},
series={Thesis},
year={1995},
publisher={University of Edinburgh, Department of Computer Science}
}
@INPROCEEDINGS{hofmann96groupoidmodel,
author = {Martin Hofmann and Thomas Streicher},
title = {The Groupoid Interpretation of Type Theory},
booktitle = {In Venice Festschrift},
year = {1996},
pages = {83--111},
publisher = {Oxford University Press}
}
@INPROCEEDINGS{Hofmann97syntaxand,
author = {Martin Hofmann},
title = {Syntax and Semantics of Dependent Types},
booktitle = {Semantics and Logics of Computation},
year = {1997},
pages = {79--130},
publisher = {Cambridge University Press}
}
@incollection{Howard80,
author = {Howard, William A.},
booktitle = {To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism},
citeulike-article-id = {5917448},
comment = {Reprint of 1969 article},
editor = {Seldin, J. P. and Hindley, J. R.},
keywords = {dissertation},
pages = {479--490},
posted-at = {2009-10-09 20:21:48},
priority = {0},
publisher = {Academic Press},
title = {{The formulas-as-types notion of construction}},
year = {1980}
}
@Misc{kapulkin12simplicial,
Author = {Chris Kapulkin and Peter LeFanu Lumsdaine and Vladimir Voevodsky},
note = {\url{http://arxiv.org/abs/1211.2851/}{arXiv:1211.2851}},
Title = {The Simplicial Model of Univalent Foundations},
Year = 2012}
@INPROCEEDINGS{Keller10regular,
author = {Gabriele Keller and Manuel M. T. Chakravarty and Roman Leshchinskiy and Simon Peyton},
title = {Regular, shape-polymorphic, parallel arrays in Haskell},
booktitle = {In Proceedings of the ACM SIGPLAN International Conference on Functional Programming, ICFP 2010},
year = {2010}
}
@unpublished{kraus13universe,
Author = {Nicolai Kraus and Christian Sattler},
Note = {\url{http://red.cs.nott.ac.uk/~ngk/universes.pdf}},
Title = {On the Hierarchy of Univalent Universes: $U_n$ is not n-Truncated},
Year = 2013}
@unpublished{kraus14reals,
Author = {Nicolai Kraus},
Title = {Non-Normalizability of {C}auchy Sequences},
note = {Unpublished},
Year = 2014
}
@book{lambek86logic,
added-at = {2008-08-17T17:02:50.000+0200},
address = {New York, NY, USA},
author = {Lambek, J. and Scott, P. J.},
biburl = {http://www.bibsonomy.org/bibtex/2e40c62fbeeb39eed4ed08c6daf494834/msn},
description = {http://www.cambridge.org/catalogue/catalogue.asp?isbn=9780521356534},
interhash = {94209269255083dce4ce08c2fb146342},
intrahash = {e40c62fbeeb39eed4ed08c6daf494834},
isbn = {0-521-24665-2},
keywords = {cites.ref state.unclassified},
publisher = {Cambridge University Press},
timestamp = {2008-08-17T17:02:50.000+0200},
title = {Introduction to higher order categorical logic},
year = 1986
}
@MISC{licatatrick,
author = {Dan Licata},
title = {Running Circles Around (In) Your Proof Assistant; or, Quotients that Compute},
note = {\url{http://homotopytypetheory.org/2011/04/23/running-circles-around-in-your-proof-assistant/}},
year = {2011}}
@MISC{lindley13hasochism,
author = {Sam Lindley and Conor Mcbride},
title = {Hasochism The Pleasure and Pain of Dependently Typed Haskell Programming},
year = {2013},
note = {Haskell Symposium 2013}
}
@article{liskov94,
author = {Barbara Liskov and
Jeannette M. Wing},
title = {A Behavioral Notion of Subtyping},
journal = {ACM Trans. Program. Lang. Syst.},
volume = {16},
number = {6},
year = {1994},
pages = {1811-1841},
ee = {http://doi.acm.org/10.1145/197320.197383},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@book{maclane98categories,
author = {Mac Lane, Saunders},
day = {25},
edition = {2nd},
howpublished = {Hardcover},
isbn = {0387984038},
keywords = {categories, functor, natural\_transformation},
month = sep,
posted-at = {2010-06-14 15:00:19},
priority = {0},
publisher = {Springer},
series = {Graduate Texts in Mathematics},
title = {{Categories for the Working Mathematician}},
url = {http://www.amazon.com/exec/obidos/redirect?tag=citeulike07-20\&path=ASIN/0387984038},
year = {1998}
}
@MISC{malatasta13smallir,
author = {Lorenzo Malatesta and Thorsten Altenkirch and Neil Ghani and Peter Hancock and Conor McBride},
title = {Small Induction Recursion, Indexed Containers and Dependent Polynomials are equivalent},
year = {2013},
note = {TLCA 2013}
}
@incollection {martinlof72,
AUTHOR = {Martin-L{\"o}f, Per},
TITLE = {An intuitionistic theory of types},
BOOKTITLE = {Twenty-five years of constructive type theory ({V}enice,
1995)},
SERIES = {Oxford Logic Guides},
VOLUME = {36},
PAGES = {127--172},
PUBLISHER = {Oxford Univ. Press, New York},
YEAR = {1998},
MRCLASS = {03B15 (03F55)},
MRNUMBER = {1686864},
}
@incollection{martinlof73predicative,
Author = {Per Martin-L{\"o}f},
Booktitle = {Logic Colloquium '73, Proceedings of the Logic Colloquium},
Editor = {H.E. Rose and J.C. Shepherdson},
Mrclass = {02C15 (02D99)},
Mrnumber = {0387009 (52 \#7856)},
Mrreviewer = {Horst Luckhardt},
Pages = {73--118},
Publisher = {North-Holland},
Series = {Studies in Logic and the Foundations of Mathematics},
Title = {An intuitionistic theory of types: predicative part},
Volume = 80,
Year = 1975}
@incollection{martinlof75models,
Author = {Per Martin-L{\"o}f},
Booktitle = {Proceedings of the Third Scandinavian Symposium},
Editor = {Stig Kanger},
Pages = {81--109},
Publisher = {North-Holland},
Title = {About models for intuitionistic type theories and the notion of definitional equality},
Series = {Studies in Logic and the Foundations of Mathematics},
Volume = 82,
Year = 1975}
@book{martinlof84sambin,
Author = {Martin-L{\"o}f, Per},
Isbn = {88-7088-105-9},
Mrclass = {03B15 (03F50 03F55)},
Mrnumber = {769301 (86j:03005)},
Mrreviewer = {M. M. Richter},
Pages = {iv+91},
Publisher = {Bibliopolis},
Series = {Studies in Proof Theory},
Subtitle = {Notes by Giovanni Sambin},
Title = {Intuitionistic type theory},
Volume = {1},
Year = {1984}}
@article{mcbride04view,
author = {McBride, Conor and McKinna, James},
title = {The View from the Left},
journal = {J. Funct. Program.},
issue_date = {January 2004},
volume = {14},
number = {1},
month = jan,
year = {2004},
issn = {0956-7968},
pages = {69--111},
numpages = {43},
url = {http://dx.doi.org/10.1017/S0956796803004829},
doi = {10.1017/S0956796803004829},
acmid = {967496},
publisher = {Cambridge University Press},
address = {New York, NY, USA},
}
@article{mcbride08applicative,
author = {Mcbride, Conor and Paterson, Ross},
title = {Applicative programming with effects},
journal = {J. Funct. Program.},
issue_date = {January 2008},
volume = {18},
number = {1},
month = jan,
year = {2008},
issn = {0956-7968},
pages = {1--13},
numpages = {13},
url = {http://dx.doi.org/10.1017/S0956796807006326},
doi = {10.1017/S0956796807006326},
acmid = {1348941},
publisher = {Cambridge University Press},
address = {New York, NY, USA},
}
@Misc{mcbride13dtmp,
Author = {Conor McBride},
Title = {Dependently typed metaprogramming (in Agda). A summer course at The University of Cambridge},
note = {\url{http://www.cl.cam.ac.uk/~ok259/agda-course-13}},
Year = 2013}
@INPROCEEDINGS{mellier95,
author = {Melli{\`e}s, Paul-Andr{\'e}},
title = {Typed lambda-calculi with explicit substitutions may not terminate},
booktitle = {Proceedings of the Second International Conference on Typed Lambda Calculi and Applications, Edinburgh},
series = {Lecture Notes in Computer Science},
volume = {902},
Pages = {328--334},
Publisher = {Springer},
year = {1995}
}
Pages 328–334 of: Tlca ’95: Proceedings of the second international conference
on typed lambda calculi and applications. London, UK: Springer-Verlag.
@book{milner97ml,
author = {Robin Milner and Mads Tofte and Robert Harper and David MacQueen},
title = {The Definition of Standard ML},
year = {1997},
publisher = {MIT Press}
}
@article{mitchell88,
author = {Mitchell, John C. and Plotkin, Gordon D.},
title = {Abstract Types Have Existential Type},
journal = {ACM Trans. Program. Lang. Syst.},
issue_date = {July 1988},
volume = {10},
number = {3},
month = jul,
year = {1988},
issn = {0164-0925},
pages = {470--502},
numpages = {33},
url = {http://doi.acm.org/10.1145/44501.45065},
doi = {10.1145/44501.45065},
acmid = {45065},
publisher = {ACM},
address = {New York, NY, USA},
}
@InProceedings{morris09indexed,
author = {Peter Morris and Thorsten Altenkirch},
title = {Indexed Containers},
year = {2009},
booktitle = {Twenty-Fourth IEEE Symposium in Logic in Computer Science (LICS 2009)},
}
@phdthesis{norell07thesis,
author = {Ulf Norell},
title = {Towards a practical programming language based on dependent type theory},
school = {Chalmers University of Technology},
year = {2007}}
@INPROCEEDINGS{Palmgren98onuniverses,
author = {Erik Palmgren},
title = {On universes in type theory},
booktitle = {Twenty-five years of constructive type theory},
series = {Oxford Logic Guides},
volume = {36},
pages = {191 – 204},
year = {1998},
publisher = {Oxford University Press}
}
@book{ PIERCE91,
author = "Benjamin C. Pierce",
title = "Basic Category Theory for Computer Scientists",
year = "1991",
publisher = mitpress,
fullisbn = "0-262-66071-7",
orderinginfo = "MIT PRESS 55 Hayward ST. Cambridge Mass 02142 USA
800-356-0343",
europeinfo = "14 Bloomsbury Square London WC1A 2LP U.K. Facsimile:
071-404-0601",
plclub = yes,
bcp = yes,
keys = "books",
}
@misc{PJH99Report,
author = {{Peyton Jones} [editor], Simon and Hughes [editor], John and Augustsson, Lennart and Barton, Dave and Boutel, Brian and Burton, Warren and Fraser, Simon and Fasel, Joseph and Hammond, Kevin and Hinze, Ralf and Hudak, Paul and J
ohnsson, Thomas and Jones, Mark and Launchbury, John and Meijer, Erik and Peterson, John and Reid, Alastair and Runciman, Colin and Wadler, Philip},
editor = {{Peyton Jones}, Simon and Hughes, John},
howpublished = {Available from \texttt{http://www.haskell.org/definition/}},
month = {February},
title = {{Haskell}~98 --- {A} Non-strict, Purely Functional Language},
year = 1999
}
@INPROCEEDINGS{pollack92implicitsyntax,
author = {Robert Pollack},
title = {Implicit Syntax},
booktitle = {Informal Proceedings of First Workshop on Logical Frameworks},
year = {1992},
pages = {pages}
}
@INPROCEEDINGS{reynolds83abstraction,
author = {John C. Reynolds},
title = {Types, Abstraction and Parametric Polymorphism},
booktitle = {Information Processing 83, Proceedings of the IFIP 9th World Computer Congress, Paris, September 19-23, 1983},
editor = {R. E. A. Mason},
publisher = {Elsevier Science Publishers B. V. (North-Holland), Amsterdam},
year = {1983},
pages = {513--523}}
@Misc{sozeau13twogroupoidmodel,
Author = {Matthieu Sozeau, Nicolas Tabareau},
note = {\url{http://hal.inria.fr/hal-00786589/en}},
Title = {Univalence for free},
Year = {2013}}
@Misc{streicher93habil,
Author = {Thomas Streicher},
note = {\url{http://www.mathematik.tu-darmstadt.de/~streicher/HabilStreicher.pdf}},
Title = {Investigations into intensional type theory. Habilitation thesis},
Year = {1993}}
@article{swierstra08alacarte,
author={Wouter Swierstra},
title={Data types \`a la carte},
journal={Journal of Functional Programming},
year={2008},
volume={18},
number={4},
pages={423--436},
month={July}
}
@book{troelstra88constructivism,
title={Constructivism in Mathematics: An Introduction},
author={Troelstra, A.S. and van Dalen, D.},
lccn={88005240},
series={Studies in logic and the foundations of mathematics},
url={http://books.google.co.uk/books?id=XfuKmgEACAAJ},
year={1988},
publisher={North-Holland}
}
@ARTICLE{Turner04totalfunctional,
author = {David Turner},
title = {Total Functional Programming},
journal = {Journal of Universal Computer Science},
year = {2004},
volume = {10},
pages = {187--209}}
@unpublished{voevodsky06veryshort,
Author = {Vladimir Voevodsky},
Date-Modified = {2013-05-12 19:02:35 +0000},
Note = {\url{http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/Hlambda_short_current.pdf}},
Title = {A very short note on the homotopy {$\lambda$}-calculus},
Year = 2006}
@article{voevodsky10grant,
Author = {Voevodsky, V.},
Journal = {a modified version of an NSF grant application},
Title = {{Univalent Foundations Project}},
Url = {www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/univalent_foundations_project.pdf},
Bdsk-Url-1 = {www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/univalent_foundations_project.pdf},
year = {2010}}
@inproceedings{wadler89theoremsforfree,
author = {Philip Wadler},
title = {Theorems for free!},
booktitle = {Functional Programming Languages and Computer Architecture},
year = {1989},
pages = {347--359},
publisher = {ACM Press}
}
@MISC{Wadler95monadsfor,
author = {Philip Wadler},
title = {Monads for functional programming},
year = {1995}
}
@misc{warren11strictomegagroupoid,
author="Warren, Michael A.",
title="{The strict $\omega$-groupoid interpretation of type theory.}",
language="English",
howpublished="{Hart, Bradd (ed.) et al., Models, logics, and higher-dimensional
categories: A tribute to the work of Mih\'aly Makkai. Proceedings of a
conference, CRM, Montr\'eal, Canada, June 18--20, 2009. Providence, RI:
American Mathematical Society (AMS). CRM Proceedings and Lecture Notes 53,
291-340 (2011).}",
year="2011",
reviewer="{Hirokazu Nishimura (Tsukuba)}",
keywords="{constructive type theory; category of small groupoids; strict
$\omega$-groupoids}",
classmath="{*03B15 (Higher-order logic)
03G30 (Categorical logic)
18D05 (2-categories and generalizations)
}",
}
@inproceedings{coincidences,
author = {Conor McBride},
title = {Outrageous but meaningful coincidences: dependent type-safe syntax
and evaluation},
booktitle = {Proceedings of the {ACM} {SIGPLAN} Workshop on Generic Programming},
pages = {1--12},
year = {2010},
crossref = {DBLP:conf/icfp/2010wgp},
doi = {10.1145/1863495.1863497},
timestamp = {Thu, 26 May 2011 19:03:24 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/icfp/McBride10},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/icfp/2010wgp,
editor = {Bruno C. d. S. Oliveira and
Marcin Zalewski},
title = {Proceedings of the {ACM} {SIGPLAN} Workshop on Generic Programming,
{WGP} 2010, Baltimore, MD, USA, September 27-29, 2010},
publisher = {{ACM}},
year = {2010},
isbn = {978-1-4503-0251-7},
timestamp = {Thu, 26 May 2011 19:03:24 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/icfp/2010wgp},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{nisse,
added-at = {2010-08-25T08:47:38.000+0200},
author = {Danielsson, Nils Anders},
bibsource = {{DBLP, http://dblp.uni-trier.de}},
biburl = {http://www.bibsonomy.org/bibtex/21dbe1359542e438b07af57ec0588a346/miguel.pagano},
booktitle = {{TYPES}},
crossref = {DBLP:conf/types/2006},
ee = {{http://dx.doi.org/10.1007/978-3-540-74464-1_7}},
interhash = {be7a1c39d076a92f52af28ea9fef0629},
intrahash = {1dbe1359542e438b07af57ec0588a346},
keywords = {imported},
pages = {93-109},
printed = {{TT}},
timestamp = {2010-08-25T08:47:43.000+0200},
title = {A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family},
year = {{2006}}
}
@proceedings{DBLP:conf/types/2006,
editor = {Thorsten Altenkirch and
Conor McBride},
title = {Types for Proofs and Programs, International Workshop, {TYPES} 2006,
Nottingham, UK, April 18-21, 2006, Revised Selected Papers},
series = {Lecture Notes in Computer Science},
volume = {4502},
publisher = {Springer},
year = {2007},
isbn = {978-3-540-74463-4},
timestamp = {Mon, 17 Sep 2007 12:52:22 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/types/2006},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{devriese,
author = {Devriese, Dominique and Piessens, Frank},
title = {Typed syntactic meta-programming},
booktitle = {Proceedings of the 2013 ACM SIGPLAN International Conference on Functional Programming (ICFP 2013)},
year = {2013},
month = {September},
pages = {73--85},
publisher = {ACM},
isbn = {978-1-4503-2326-0},
url = {https://lirias.kuleuven.be/handle/123456789/404549},
doi = {10.1145/2500365.2500575},
}
@article{Palsberg,
author = {Brown, Matt and Palsberg, Jens},
title = {Self-Representation in {G}irard's {S}ystem {U}},
journal = {SIGPLAN Not.},
issue_date = {January 2015},
volume = {50},
number = {1},
month = jan,
year = {2015},
issn = {0362-1340},
pages = {471--484},
numpages = {14},
url = {http://doi.acm.org/10.1145/2775051.2676988},
doi = {10.1145/2775051.2676988},
acmid = {2676988},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {lambda calculus, languages, self representation, theory, types},
}
@inproceedings{jaber:hal-01319066,
TITLE = {{The Definitional Side of the Forcing}},
AUTHOR = {Jaber, Guilhem and Lewertowski, Gabriel and P{\'e}drot, Pierre-Marie and Sozeau, Matthieu and Tabareau, Nicolas},
URL = {https://hal.archives-ouvertes.fr/hal-01319066},
BOOKTITLE = {{Logics in Computer Science}},
ADDRESS = {New York, United States},
YEAR = {2016},
MONTH = May,
DOI = {10.1145/http://dx.doi.org/10.1145/2933575.2935320},
KEYWORDS = {Effects ; Coq ; Forcing ; Dependent type theory ; Inductive types},
PDF = {https://hal.archives-ouvertes.fr/hal-01319066/file/main.pdf},
HAL_ID = {hal-01319066},
HAL_VERSION = {v1},
}
@Unpublished{pitts:private,
author = {Andrew Pitts},
title = {Quotient types in {Agda}},
note = {Private email},
OPTkey = {},
month = {May},
year = {2015},
OPTannote = {}
}
@PhdThesis{kraus:phd,
author = {Nicolai Kraus},
title = {Truncation Levels in Homotopy Type Theory},
school = {University of Nottingham},
year = {2015},
OPTkey = {},
OPTtype = {},
OPTaddress = {},
OPTmonth = {},
OPTnote = {},
OPTannote = {}
}
@misc{agdawiki,
author = {{The Agda development team}},
title = {{Agda}},
url = {http://wiki.portal.chalmers.se/agda},
year = {2015}
}
@article{hedberg,
title={A coherence theorem for {M}artin-{L}{\"o}f's type theory},
author={Hedberg, Michael},
journal={Journal of Functional Programming},
volume={8},
number={04},
pages={413--436},
year={1998},
publisher={Cambridge Univ Press}
}
@ARTICLE{debruijn,
author = {N. G. De Bruijn},
title = {Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser Theorem},
journal = {INDAG. MATH},
year = {1972},
volume = {34},
pages = {381--392}
}
@article{hereditary,
abstract = {{We present the propositional fragment CLF 0 of the Concurrent Logical Framework (CLF). CLF extends the Linear Logical Framework to allow the natural representation of concurrent computations in an object language. The underlying type theory uses monadic types to segregate values from computations. This separation leads to a tractable notion of definitional equality that identifies computations differing only in the order of execution of independent steps. From a logical point of view our type theory can be seen as a novel combination of lax logic and dual intuitionistic linear logic. An encoding of a small Petri net exemplifies the representation methodology, which can be summarized as ” concurrent computations as monadic expressions”.}},
author = {Watkins, Kevin and Cervesato, Iliano and Pfenning, Frank and Walker, David},
citeulike-article-id = {5802354},
citeulike-linkout-0 = {http://www.springerlink.com/content/fwlrpm102djtlaeb},
journal = {Types for Proofs and Programs},
keywords = {concurrency, hereditary-substitution, linear-logic, logical-frameworks},
pages = {355--377},
posted-at = {2014-07-29 16:56:16},
priority = {0},
title = {{A Concurrent Logical Framework: The Propositional Fragment}},
url = {http://www.springerlink.com/content/fwlrpm102djtlaeb},
year = {2004}
}
@MISC{chantal,
author = {Chantal Keller and Thorsten Altenkirch},
title = {Normalization by hereditary substitutions},
year = {}
}
@PhdThesis{conorthesis,
author = "Conor McBride",
title = "Dependently typed functional programs and their proofs",
school = "University of Edinburgh",
year = 1999
}
@inproceedings{cockx,
author = {Cockx, Jesper and Devriese, Dominique and Piessens, Frank},
title = {Pattern Matching Without K},
booktitle = {Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming},
series = {ICFP '14},
year = {2014},
isbn = {978-1-4503-2873-9},
location = {Gothenburg, Sweden},
pages = {257--268},
numpages = {12},
url = {http://doi.acm.org/10.1145/2628136.2628139},
doi = {10.1145/2628136.2628139},
acmid = {2628139},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {agda, dependent pattern matching, homotopy type theory, k axiom},
}
@inproceedings{hofmann95conservativity,
author = {Martin Hofmann},
title = {Conservativity of Equality Reflection over Intensional Type
Theory.},
booktitle = {TYPES 95},
year = {1995},
pages = {153-164},
}
@inproceedings{martinlof85constructive,
author = {Martin-L\"{o}f, Per},
title = {Constructive Mathematics and Computer Programming},
booktitle = {Proc. Of a Discussion Meeting of the Royal Society of London on Mathematical Logic and Programming Languages},
year = {1985},
isbn = {0-13-561465-1},
location = {London, United Kingdom},
pages = {167--184},
numpages = {18},
url = {http://dl.acm.org/citation.cfm?id=3721.3731},
acmid = {3731},
publisher = {Prentice-Hall, Inc.},
address = {Upper Saddle River, NJ, USA},
}
@InProceedings{alti:lics99,
author = {Thorsten Altenkirch},
title = {Extensional Equality in Intensional Type Theory},
booktitle = {14th Symposium on Logic in Computer Science},
year = {1999},
pages = { 412 -- 420 }
}
@book{nuprl,
author = {Constable, R. L. and Allen, S. F. and Bromley, H. M. and Cleaveland, W. R. and Cremer, J. F. and Harper, R. W. and Howe, D. J. and Knoblock, T. B. and Mendler, N. P. and Panangaden, P. and Sasaki, J. T. and Smith, S. F.},
title = {Implementing Mathematics with the Nuprl Proof Development System},
year = {1986},
isbn = {0-13-451832-2},
publisher = {Prentice-Hall, Inc.},
address = {Upper Saddle River, NJ, USA},
}
@inproceedings{notanumber,
author = {McBride, Conor and McKinna, James},
title = {Functional Pearl: I Am Not a Number --- {I} Am a Free Variable},
booktitle = {Proceedings of the 2004 ACM SIGPLAN Workshop on Haskell},
series = {Haskell '04},
year = {2004},
isbn = {1-58113-850-4},
location = {Snowbird, Utah, USA},
pages = {1--9},
numpages = {9},
url = {http://doi.acm.org/10.1145/1017472.1017477},
doi = {10.1145/1017472.1017477},
acmid = {1017477},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {abstract syntax, bound variables, de Bruijn representation, free variables, fresh names, haskell, implementing epigram, induction principles},
}
@ARTICLE{Dybjer97inductivefamilies,
author = {Peter Dybjer},
title = {Inductive Families},
journal = {Formal Aspects of Computing},
year = {1997},
volume = {6},
pages = {440--465}
}
@inproceedings{paulinmohring,
author = {Christine Paulin{-}Mohring},
title = {Inductive Definitions in the system {C}oq --- Rules and Properties},
booktitle = {Typed Lambda Calculi and Applications, International Conference on
Typed Lambda Calculi and Applications, {TLCA} '93, Utrecht, The Netherlands,
March 16-18, 1993, Proceedings},
pages = {328--345},
year = {1993},
crossref = {DBLP:conf/tlca/1993},
doi = {10.1007/BFb0037116},
timestamp = {Tue, 14 Jun 2011 20:35:53 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/tlca/Paulin-Mohring93},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/tlca/1993,
editor = {Marc Bezem and
Jan Friso Groote},
title = {Typed Lambda Calculi and Applications, International Conference on
Typed Lambda Calculi and Applications, {TLCA} '93, Utrecht, The Netherlands,
March 16-18, 1993, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {664},
publisher = {Springer},
year = {1993},
isbn = {3-540-56517-5},
timestamp = {Fri, 28 Feb 2003 07:51:21 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/tlca/1993},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{alti:catind2,
author = {Thorsten Altenkirch and
Peter Morris and
Fredrik Nordvall Forsberg and
Anton Setzer},
title = {A Categorical Semantics for Inductive-Inductive Definitions},
booktitle = {CALCO},
year = {2011},
pages = {70-84},
ee = {http://dx.doi.org/10.1007/978-3-642-22944-2_6},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{ttintt,
author = {Thorsten Altenkirch and
Ambrus Kaposi},
title = {Type theory in type theory using quotient inductive types},
booktitle = {Proceedings of the 43rd Annual {ACM} {SIGPLAN-SIGACT} Symposium on
Principles of Programming Languages, {POPL} 2016, St. Petersburg,
FL, USA, January 20 - 22, 2016},
pages = {18--29},
year = {2016},
crossref = {DBLP:conf/popl/2016},
doi = {10.1145/2837614.2837638},
timestamp = {Fri, 08 Jan 2016 18:18:25 +0100},
biburl = {http://dblp2.uni-trier.de/rec/bib/conf/popl/AltenkirchK16},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/popl/2016,
editor = {Rastislav Bodik and
Rupak Majumdar},
title = {Proceedings of the 43rd Annual {ACM} {SIGPLAN-SIGACT} Symposium on
Principles of Programming Languages, {POPL} 2016, St. Petersburg,
FL, USA, January 20 - 22, 2016},
publisher = {{ACM}},
year = {2016},
isbn = {978-1-4503-3549-2},
timestamp = {Fri, 08 Jan 2016 18:18:25 +0100},
biburl = {http://dblp2.uni-trier.de/rec/bib/conf/popl/2016},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@book{nuo,
title={Quotient types in type theory},
author={Nuo Li},
series={Thesis},
url={http://eprints.nottingham.ac.uk/28941},
year={2015},
publisher={University of Nottingham, Department of Computer Science}
}
@inproceedings{sojakova,
author = {Sojakova, Kristina},
title = {Higher Inductive Types As Homotopy-Initial Algebras},
booktitle = {Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
series = {POPL '15},
year = {2015},
isbn = {978-1-4503-3300-9},
location = {Mumbai, India},
pages = {31--42},
numpages = {12},
doi = {10.1145/2676726.2676983},
acmid = {2676983},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {higher inductive type, homotopy type theory, homotopy-initial algebra, w-suspension},
}
@article{Sojakova:2015:HIT:2775051.2676983,
author = {Sojakova, Kristina},
title = {Higher Inductive Types As Homotopy-Initial Algebras},
journal = {SIGPLAN Not.},
issue_date = {January 2015},
volume = {50},
number = {1},
month = jan,
year = {2015},
issn = {0362-1340},
pages = {31--42},
numpages = {12},
doi = {10.1145/2775051.2676983},
acmid = {2676983},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {higher inductive type, homotopy type theory, homotopy-initial algebra, w-suspension},
}
@MISC{paoloHIT,
author = {Paolo Capriotti},
title = {Mutual and Higher Inductive Types in Homotopy Type Theory},
year = {2014},
note = {Nottingham FP Lab Away Day}
}
@inproceedings{lean,
author = {Leonardo Mendon{\c{c}}a de Moura and
Soonho Kong and
Jeremy Avigad and
Floris van Doorn and
Jakob von Raumer},
title = {The {L}ean Theorem Prover (System Description)},
booktitle = {Automated Deduction - {CADE-25} - 25th International Conference on
Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings},
pages = {378--388},
year = {2015},
crossref = {DBLP:conf/cade/2015},
url = {http://dx.doi.org/10.1007/978-3-319-21401-6_26},
doi = {10.1007/978-3-319-21401-6_26},
timestamp = {Fri, 31 Jul 2015 13:18:27 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/cade/MouraKADR15},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/2015,
editor = {Amy P. Felty and
Aart Middeldorp},
title = {Automated Deduction - {CADE-25} - 25th International Conference on
Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9195},
publisher = {Springer},
year = {2015},
url = {http://dx.doi.org/10.1007/978-3-319-21401-6},
doi = {10.1007/978-3-319-21401-6},
isbn = {978-3-319-21400-9},
timestamp = {Fri, 31 Jul 2015 13:15:07 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/cade/2015},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@INPROCEEDINGS{schaefer,
title = {Completeness and Decidability of de {B}ruijn Substitution Algebra in {C}oq},
author = {Steven Sch{\"a}fer and Gert Smolka and Tobias Tebbi},
year = {2015},
publisher = {ACM},
booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015},
pages = {67-73},
}
@inproceedings{atkey,
author = {Robert Atkey and
Neil Ghani and
Patricia Johann},
title = {A relationally parametric model of dependent type theory},
booktitle = {The 41st Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of
Programming Languages, {POPL} '14, San Diego, CA, USA, January 20-21,
2014},
pages = {503--516},
year = {2014},
crossref = {DBLP:conf/popl/2014},
doi = {10.1145/2535838.2535852},
timestamp = {Thu, 09 Jan 2014 08:32:32 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/popl/AtkeyGJ14},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/popl/2014,
editor = {Suresh Jagannathan and
Peter Sewell},
title = {The 41st Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of
Programming Languages, {POPL} '14, San Diego, CA, USA, January 20-21,
2014},
publisher = {{ACM}},
year = {2014},
isbn = {978-1-4503-2544-8},
timestamp = {Thu, 09 Jan 2014 08:21:22 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/popl/2014},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@techreport{plotkin73,
author = "Plotkin, Gordon D.",
title = "Lambda-Definability and Logical Relations",
type = "Memorandum",
number = "SAI--RM--4",
institution = "University of Edinburgh",
department = "School of Artificial Intelligence",
address = "Edinburgh, Scotland",
month = "October",
year = "1973",
filename = "plotkin/plotkin-logical-relations",
checked = "30 April 1991"}
@article{ghaniFibrationalInduction,
author = {Neil Ghani and
Patricia Johann and
Cl{\'{e}}ment Fumex},
title = {Generic Fibrational Induction},
journal = {Logical Methods in Computer Science},
volume = {8},
number = {2},
year = {2012},
url = {http://dx.doi.org/10.2168/LMCS-8(2:12)2012},
doi = {10.2168/LMCS-8(2:12)2012},
timestamp = {Mon, 15 Oct 2012 13:17:50 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/abs-1206-0357},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@book{crole,
title = "Categories for types",
author = "Crole, Roy L.",
series = "Cambridge mathematical textbooks",
publisher = "Cambridge University Press",
address = "Cambridge, New York",
url = "http://opac.inria.fr/record=b1088776",
isbn = "0-521-45092-6",
year = 1993
}
@book{bird,
author = {Bird, Richard and de Moor, Oege},
title = {Algebra of Programming},
year = {1997},
isbn = {0-13-507245-X},
publisher = {Prentice-Hall, Inc.},
address = {Upper Saddle River, NJ, USA},
}
@INPROCEEDINGS{cockxsprinkles,
title = {Sprinkles of extensionality for your vanilla type theory},
author = {Cockx, Jesper and Abel, Andreas},
year = {2016},
booktitle = {22nd International Conference on Types for Proofs and Programs, TYPES 2016},
editor = {Ghilezan, Silvia and Ivetić Jelena},
publisher = {University of Novi Sad},
comment = {Abstract}
}
@INPROCEEDINGS{bassel,
title = {On the Decidability of Conversion in Type Theory},
author = {Abel, Andreas and Coquand, Thierry and Mannaa, Bassel},
year = {2016},
booktitle = {22nd International Conference on Types for Proofs and Programs, TYPES 2016},
editor = {Ghilezan, Silvia and Ivetić Jelena},
publisher = {University of Novi Sad},
comment = {Abstract}
}
@inproceedings{twelf,
address = {Trento, Italy},
author = {Pfenning, Frank and Sch{\"{u}}rmann, Carsten},
booktitle = {Proceedings of the 16th International Conference on Automated Deduction (CADE-16)},
citeulike-article-id = {5893175},
editor = {Ganzinger, H.},
keywords = {elf, file-import-09-10-05b, lf, twelf},
month = jul,
pages = {202--206},
posted-at = {2009-10-05 21:42:23},
priority = {2},
publisher = {Springer-Verlag LNAI 1632},
title = {System Description: {T}welf --- A Meta-Logical Framework for Deductive Systems},
year = {1999}
}
@phdthesis{chapmanthesis,
author = {James Chapman},
title = {Type checking and normalisation},
school = {University of Nottingham},
year = {2008}}
@inproceedings{palsberg2016,
author = {Brown, Matt and Palsberg, Jens},
title = {Breaking Through the Normalization Barrier: A Self-interpreter for {F}-omega},
booktitle = {Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
series = {POPL '16},
year = {2016},
isbn = {978-1-4503-3549-2},
location = {St. Petersburg, FL, USA},
pages = {5--17},
numpages = {13},
url = {http://doi.acm.org/10.1145/2837614.2837623},
doi = {10.1145/2837614.2837623},
acmid = {2837623},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {Lambda Calculus, Meta Programming, Self Interpretation, Self Representation},
}
@book{danvy1999type,
title={Type-directed partial evaluation},
author={Danvy, Olivier},
year={1999},
publisher={Springer}
}
@inproceedings{abel2007normalization,
title={Normalization by evaluation for {Martin-L\"of} type theory with typed equality judgements},
author={Abel, Andreas and Coquand, Thierry and Dybjer, Peter},
booktitle={Logic in Computer Science, 2007. LICS 2007. 22nd Annual IEEE Symposium on},
pages={3--12},
year={2007},
organization={IEEE}
}
@incollection{abel2010towards,
title={Towards Normalization by Evaluation for the $\beta$$\eta$-Calculus of Constructions},
author={Abel, Andreas},
booktitle={Functional and Logic Programming},
pages={224--239},
year={2010},
publisher={Springer}
}
@InProceedings{alti:ctcs95,
author = "Thorsten Altenkirch and Martin Hofmann and Thomas Streicher",
title = "Categorical reconstruction of a reduction free
normalization proof",
year = "1995",
booktitle = "Category Theory and Computer Science",
editor = {David Pitt and David E. Rydeheard and Peter Johnstone},
series = {LNCS 953},
pages = {182-199},
}
@InProceedings{alti:lics96,
author = "Thorsten Altenkirch and Martin Hofmann and Thomas Streicher",
title = "Reduction-free normalisation for a polymorphic system",
pages = "98-106",
booktitle = "11th Annual IEEE Symposium on Logic in Computer
Science",
year = "1996",
}
@Unpublished{alti:f97,
author = {Thorsten Altenkirch and Martin Hofmann and Thomas Streicher},
title = {Reduction-free normalisation for system {$F$}},
note = {Unpublished draft},
year = {1997},
www = {http://www.cs.nott.ac.uk/~txa/publ/f97.pdf},
}
@InProceedings{alti:lics01,
author = "Thorsten Altenkirch and Peter Dybjer and Martin Hofmann and Phil Scott",
title = "Normalization by evaluation for typed lambda calculus with
coproducts",
pages = "303-310",
booktitle = "16th Annual IEEE Symposium on Logic in Computer
Science",
year = "2001"
}
@article{tait1967,
author = "Tait, W. W.",
fjournal = "Journal of Symbolic Logic",
journal = "J. Symbolic Logic",
month = "06",
number = "2",
pages = "198--212",
publisher = "Association for Symbolic Logic",
title = "Intensional Interpretations of Functionals of Finite Type I",
url = "http://projecteuclid.org/euclid.jsl/1183735831",
volume = "32",
year = "1967"
}
@incollection{plotkin80,
address = {London},
author = {Plotkin, Gordon D.},
booktitle = {To H.B.\~{}Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism},
citeulike-article-id = {2765456},
editor = {Seldin, J. P. and Hindley, J. R.},
keywords = {rcb-bibfile},
posted-at = {2008-05-07 12:57:39},
priority = {2},
publisher = {Academic Press},
title = {Lambda-Definability in the Full Type Hierarchy},
year = {1980}
}
@article{statman,
author = {Richard Statman},
title = {Completeness, Invariance and lambda-Definability},
journal = {J. Symb. Log.},
volume = {47},
number = {1},
pages = {17--26},
year = {1982},
url = {http://dx.doi.org/10.2307/2273377},
doi = {10.2307/2273377},
timestamp = {Tue, 05 Aug 2014 16:36:24 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/jsyml/Statman82},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@Inbook{plotkinabadi,
author="Plotkin, Gordon
and Abadi, Mart{\'i}n",
editor="Bezem, Marc
and Groote, Jan Friso",
title="A logic for parametric polymorphism",
bookTitle="Typed Lambda Calculi and Applications: International Conference on Typed Lambda Calculi and Applications TLCA '93 March, 16--18, 1993, Utrech, The Netherlands Proceedings",
year="1993",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="361--375",
isbn="978-3-540-47586-6",
doi="10.1007/BFb0037118",
url="http://dx.doi.org/10.1007/BFb0037118"
}
@article{udayReynolds,
title = "Logical Relations and Parametricity --– A {R}eynolds Programme for Category Theory and Programming Languages ",
journal = "Electronic Notes in Theoretical Computer Science",
volume = "303",
number = "0",
pages = "149 - 180",
year = "2014",
note = "Proceedings of the Workshop on Algebra, Coalgebra and Topology (WACT 2013) ",
issn = "1571-0661",
doi = "http://dx.doi.org/10.1016/j.entcs.2014.02.008",
url = "http://www.sciencedirect.com/science/article/pii/S1571066114000346",
author = "Claudio Hermida and Uday S. Reddy and Edmund P. Robinson",
keywords = "Universal algebra",
keywords = "Category Theory",
keywords = "Homomorphisms",
keywords = "Logical Relations",
keywords = "Natural Transformations",
keywords = "Parametric polymorphism",
keywords = "Relational Parametricity",
keywords = "Data abstraction",
keywords = "Information hiding",
keywords = "Definability",
keywords = "Reflexive Graphs",
keywords = "Fibrations",
keywords = "Relation lifting "
}
@inproceedings{moulin12internalparametricity,
author = {Bernardy, Jean-Philippe and Moulin, Guilhem},
title = {A Computational Interpretation of Parametricity},
booktitle = {Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer Science},
series = {LICS '12},
year = {2012},
isbn = {978-0-7695-4769-5},
location = {New Orleans, Louisiana},
pages = {135--144},
numpages = {10},
url = {http://dx.doi.org/10.1109/LICS.2012.25},
doi = {10.1109/LICS.2012.25},
acmid = {2359499},
publisher = {IEEE Computer Society},
address = {Washington, DC, USA},
keywords = {Type structure, Lambda Calculus},
}
@book{Moulin2013,
author={Moulin, Guilhem},
title={Pure type systems with an internalized parametricity theorem},
publisher={Chalmers University of Technology},
place={G{\"o}teborg},
year={2013},
keywords={Polymorphism, Parametricity, Type structure, Lambda Calculus.},
note={Licentiate thesis}
}
@book{Moulin2016,
author={Moulin, Guilhem},
title={Internalizing Parametricity},
isbn={978-91-7597-384-5},
publisher={Chalmers University of Technology},
place={G{\"o}teborg},
year={2016},
note={PhD thesis}
}
@article{moulinpresheaf,
author = {Bernardy, Jean-Philippe and Coquand, Thierry and Moulin, Guilhem},
title = {A Presheaf Model of Parametric Type Theory},
journal = {Electronic Notes in Theoretical Computer Science},
issue_date = {December 2015},
volume = {319},
number = {C},
month = dec,
year = {2015},
issn = {1571-0661},
pages = {67--82},
numpages = {16},
url = {http://dx.doi.org/10.1016/j.entcs.2015.12.006},
doi = {10.1016/j.entcs.2015.12.006},
acmid = {2875604},
publisher = {Elsevier Science Publishers B. V.},
address = {Amsterdam, The Netherlands, The Netherlands},
keywords = {Parametricity, Presheaf semantics, Type theory},
}
@inproceedings{bernardy13color,
author = {Bernardy, Jean-Philippe and Moulin, Guilhem},
title = {Type-theory in Color},
booktitle = {Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming},
series = {ICFP '13},
year = {2013},
isbn = {978-1-4503-2326-0},
location = {Boston, Massachusetts, USA},
pages = {61--72},
numpages = {12},
url = {http://doi.acm.org/10.1145/2500365.2500577},
doi = {10.1145/2500365.2500577},
acmid = {2500577},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {erasure, parametricity, type-theory},
}
@Inbook{Oury2005,
author="Oury, Nicolas",
editor="Hurd, Joe
and Melham, Tom",
title="Extensionality in the calculus of constructions",
bookTitle="Theorem Proving in Higher Order Logics: 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005. Proceedings",
year="2005",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="278--293",
isbn="978-3-540-31820-0",
doi="10.1007/11541868_18",
url="http://dx.doi.org/10.1007/11541868_18"
}
@InProceedings{nbe,
author = {Thorsten Altenkirch and Ambrus Kaposi},
title = {Normalisation by Evaluation for Dependent Types},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {6:1--6:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Delia Kesner and Brigitte Pientka},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2016/5972},
URN = {urn:nbn:de:0030-drops-59727},
doi = {http://dx.doi.org/10.4230/LIPIcs.FSCD.2016.6},
annote = {Keywords: normalisation by evaluation, dependent types, internal type theory, logical relations, Agda}
}
@Unpublished{withoutInterval,
author = {Thorsten Altenkirch and Ambrus Kaposi},
title = {Towards a cubical type theory without an interval},
note = {Unpublished draft},
year = 2016}
@Unpublished{nbc,
author = {Thorsten Altenkirch},
title = {Normalisation by Completeness},
note = {Talk given at the Workshop on Normalization by Evaluation in Los Angeles},
url = {http://www.cs.nott.ac.uk/~psztxa/talks/nbe09.pdf},
month = {August},
year = {2009},
}
@article{shulman:invdia,
author = {Shulman, Michael},
title = {Univalence for inverse diagrams and homotopy canonicity},
journal = {Mathematical Structures in Computer Science},
note = {arXiv:1203.3253},
volume = {25},
issue = {Special Issue 05},
month = {6},
year = {2015},
issn = {1469-8072},
pages = {1203--1277},
numpages = {75},
doi = {10.1017/S0960129514000565},
URL = {http://journals.cambridge.org/article_S0960129514000565},
}
@article{lasson,
title = "Canonicity of Weak $\omega$-groupoid Laws Using Parametricity Theory",
journal = "Electronic Notes in Theoretical Computer Science",
volume = "308",
number = "",
pages = "229 - 244",
year = "2014",
note = "",
issn = "1571-0661",
doi = {10.1016/j.entcs.2014.10.013},
author = "Marc Lasson",
keywords = "type theory",
keywords = "parametricity",
keywords = "loop spaces",
keywords = "groupoids",
keywords = "identity types"
}
@article{dybjerInductive,
author = {Peter Dybjer},
title = {Representing Inductively Defined Sets by Wellorderings in Martin-L{\"{o}}f's
Type Theory},
journal = {Theor. Comput. Sci.},
volume = {176},
number = {1-2},
pages = {329--335},
year = {1997},
url = {https://doi.org/10.1016/S0304-3975(96)00145-4},
doi = {10.1016/S0304-3975(96)00145-4},
timestamp = {Sun, 28 May 2017 13:20:06 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/tcs/Dybjer97},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{lumsdaineShulman, title={Semantics of higher inductive types}, DOI={10.1017/S030500411900015X}, journal={Mathematical Proceedings of the Cambridge Philosophical Society}, publisher={Cambridge University Press}, author={Lumsdaine, Peter LeFanu and Shulman, Michael}, pages={1–50}}
@article{twolevel,
author = {Danil Annenkov and Paolo Capriotti and Nicolai Kraus and Christian Sattler},
journal = {ArXiv e-prints},
month = {may},
title = {Two-Level Type Theory and Applications},
year = {2019},
url = {http://arxiv.org/abs/1705.03307},
}
@INPROCEEDINGS{andromeda,
title = {Design and Implementation of the Andromeda proof assistant},
author = {Bauer, Andrej and Gilbert, Ga{\"e}tan and Haselwarter, Philipp and Pretnar, Matija and Stone, Christopher A.},
year = {2016},
booktitle = {22nd International Conference on Types for Proofs and Programs, TYPES 2016},
editor = {Ghilezan, Silvia and Ivetić Jelena},
publisher = {University of Novi Sad},
comment = {Abstract}
}
@book{Norell:2007thesis,
title={Towards a practical programming language based on dependent type theory},
author={Norell, Ulf},
volume={32},
year={2007},
publisher={Citeseer}
}
@online{agdadocs,
author = {Agda developers},
title = {Agda documentation},
year = {2021},
url = {https://agda.readthedocs.io/en/v2.6.1.3/},
urldate = {2021-02-17}
}
@online{leanmanual,
author = {Lean developers},
title = {Lean Reference Manual, Version 3.3},
year = {2021},
url = {https://leanprover.github.io/reference/lean_reference.pdf},
urldate = {2021-02-17}
}
@online{idrisdocs,
author = {The Idris Community},
title = {Documentation for the Idris Language},
year = {2021},
url = {http://docs.idris-lang.org/en/latest/index.html},
urldate = {2021-02-17}
}
@book{Stump:agdabook,
author = {Stump, Aaron},
title = {Verified Functional Programming in Agda},
year = {2016},
isbn = {978-1-97000-127-3},
publisher = {Association for Computing Machinery and Morgan \&\#38; Claypool},
address = {New York, NY, USA},
}
@article{brady2013idris,
title={Idris, a general-purpose dependently typed programming language: Design and implementation},
author={Brady, Edwin},
journal={Journal of Functional Programming},
volume={23},
number={05},
pages={552--593},
year={2013},
publisher={Cambridge University Press}
}
@article{mcbride2008applicative,
title={Applicative programming with effects},
author={McBride, Conor and Paterson, Ross},
journal={Journal of functional programming},
volume={18},
number={01},
pages={1--13},
year={2008},
publisher={Cambridge Univ Press}
}
@article{benton2012strongly,
title={Strongly typed term representations in Coq},
author={Benton, Nick and Hur, Chung-Kil and Kennedy, Andrew J and McBride, Conor},
journal={Journal of automated reasoning},
volume={49},
number={2},
pages={141--159},
year={2012},
publisher={Springer Netherlands}
}
@inproceedings{autosubst,
author = {Steven Sch{\"{a}}fer and
Tobias Tebbi and
Gert Smolka},
editor = {Christian Urban and
Xingyuan Zhang},
title = {Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions},
booktitle = {Interactive Theorem Proving - 6th International Conference, {ITP}
2015, Nanjing, China, August 24-27, 2015, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9236},
pages = {359--374},
publisher = {Springer},
year = {2015},
url = {https://doi.org/10.1007/978-3-319-22102-1\_24},
doi = {10.1007/978-3-319-22102-1\_24},
timestamp = {Tue, 14 May 2019 10:00:37 +0200},
biburl = {https://dblp.org/rec/conf/itp/SchaferTS15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{altenkirch1995categorical,
title={Categorical reconstruction of a reduction free normalization proof},
author={Altenkirch, Thorsten and Hofmann, Martin and Streicher, Thomas},
booktitle={Category Theory and Computer Science},
pages={182--199},
year={1995},
organization={Springer}
}
@inproceedings{altenkirch2016normalisation,
title={Normalisation by evaluation for dependent types},
author={Altenkirch, Thorsten and Kaposi, Ambrus},
booktitle={LIPIcs-Leibniz International Proceedings in Informatics},
volume={52},
year={2016},
organization={Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik}
}
@book{pierce2002types,
title={Types and programming languages},
author={Pierce, Benjamin C},
year={2002},
publisher={MIT press}
}
@book{harper2016practical,
title={Practical foundations for programming languages},
author={Harper, Robert},
year={2016},
publisher={Cambridge University Press}
}
@article{altenkirch2009big,
title={Big-step normalisation},
author={Altenkirch, Thorsten and Chapman, James},
journal={Journal of Functional Programming},
volume={19},
number={3-4},
pages={311--333},
year={2009},
publisher={Cambridge Univ Press}
}
@online{mcbride2015datatypes,
title={Datatypes of Datatypes},
author={McBride, Conor},
year={2015},
url= {http://staff.mmcs.sfedu.ru/~ulysses/Edu/SSGEP/conor/conor.pdf},
urladte = {2017-04-07}
}
@misc{augustsson1999exercise,
title={An exercise in dependent types: A well-typed interpreter},
author={Augustsson, Lennart and Carlsson, Magnus},
publisher={\url{https://pdfs.semanticscholar.org/5dae/20b002f4e9d91e60db6af192c69d7fe764c6.pdf}},
year={1999}
}
@article{coquand1997intuitionistic,
title={Intuitionistic model constructions and normalization proofs},
author={Coquand, Thierry and Dybjer, Peter},
journal={Mathematical Structures in Computer Science},
volume={7},
number={1},
pages={75--94},
year={1997},
publisher={Citeseer}
}
@article{martin1975intuitionistic,
title={An intuitionistic theory of types: Predicative part},
author={Martin-L{\"o}f, Per},
journal={Studies in Logic and the Foundations of Mathematics},
volume={80},
pages={73--118},
year={1975},
publisher={Elsevier}
}
@inproceedings{berger1991inverse,
title={An inverse of the evaluation functional for typed lambda-calculus},
author={Berger, Ulrich and Schwichtenberg, Helmut},
booktitle={Logic in Computer Science, 1991. LICS'91., Proceedings of Sixth Annual IEEE Symposium on},
pages={203--211},
year={1991},
organization={IEEE}
}
@phdthesis{abel2013normalization,
title={Normalization by Evaluation: Dependent Types and Impredicativity},
author={Abel, Andreas},
year={2013},
note = {Habilitation thesis},
school={Ludwig-Maximilians-Universit{\"a}t M{\"u}nchen}
}
@article{coquand2002formalised,
title={A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions},
author={Coquand, Catarina},
journal={Higher-Order and Symbolic Computation},
volume={15},
number={1},
pages={57--90},
year={2002},
publisher={Springer}
}
@inproceedings{altenkirch2007observational,
title={Observational equality, now!},
author={Altenkirch, Thorsten and McBride, Conor and Swierstra, Wouter},
booktitle={Proceedings of the 2007 workshop on Programming languages meets program verification},
pages={57--68},
year={2007},
organization={ACM}
}
@book{streicher1993investigations,
title={Investigations into intensional type theory},
author={Streicher, Thomas},
year={1993},
publisher={\url{http://www.mathematik.tu-darmstadt.de/~streicher/HabilStreicher.pdf}}
}
@online{agda-stdlib,
author = {Agda developers},
title = {Agda standard library},
year = 2017,
url = {https://github.com/agda/agda-stdlib},
urldate = {2017-03-10}
}
@inproceedings{coquand1992proof,
title={A proof of normalization for simply typed lambda calculus written in ALF},
author={Coquand, Catarina},
booktitle={Proceedings of the Workshop on Types for Proofs and Programs},
pages={85--92},
year={1992},
organization={Citeseer}
}
@article{bove2005modelling,
title={Modelling general recursion in type theory},
author={Bove, Ana and Capretta, Venanzio},
journal={Mathematical Structures in Computer Science},
volume={15},
number={04},
pages={671--708},
year={2005},
publisher={Cambridge Univ Press}
}
@online{initialCwF,
author = {Simon Castellan},
title = {Dependent type theory as the initial category with families},
year = 2014,
url = {http://iso.mor.phis.me/archives/2011-2012/stage-2012-goteburg/report.pdf},
urldate = {2017-03-10}
}
@inproceedings{altenkirch2009normalisation,
title={Normalisation by completeness},
author={Altenkirch, Thorsten},
booktitle={Talk given at the Workshop on Normalization by Evaluation in Los Angeles},
year={2009}
}
@online{stlc-nbe,
author = {András Kovács},
title = {Correctness of normalization-by-evaluation for STLC},
year = 2017,
url = {https://github.com/AndrasKovacs/stlc-nbe},
urldate = {2017-04-07}
}
@online{presheaf-ccc,
author = {nLab contributors},
title = {closed monoidal structure on presheaves},
year = 2017,
url = {https://ncatlab.org/nlab/show/closed+monoidal+structure+on+presheaves},
urldate = {2017-04-07}
}
@online{preorder,
author = {nLab contributors},
title = {preorder},
year = 2017,
url = {https://ncatlab.org/nlab/show/preorder},
urldate = {2017-04-07}
}
@online{wide-subcategory,
author = {nLab contributors},
title = {wide subcategory},
year = 2017,
url = {https://ncatlab.org/nlab/show/wide+subcategory},
urldate = {2017-04-07}
}
@online{intrinsic-sysF-nbe,
author = {András Kovács},
title = {Normalization by evaluation for intrinsic System F},
year = 2017,
url = {https://github.com/AndrasKovacs/sysF-NbE},
urldate = {2017-04-07}
}
@inproceedings{needle-knot,
author = {Keuchel, Steven and Weirich, Stephanie and Schrijvers, Tom},
title = {Needle \& Knot: Binder Boilerplate Tied Up},
booktitle = {Proceedings of the 25th European Symposium on Programming Languages and Systems - Volume 9632},
year = {2016},
isbn = {978-3-662-49497-4},
pages = {419--445},
numpages = {27},
url = {http://dx.doi.org/10.1007/978-3-662-49498-1_17},
doi = {10.1007/978-3-662-49498-1_17},
acmid = {2958897},
publisher = {Springer-Verlag New York, Inc.},
address = {New York, NY, USA},
}
@article{goguen2006eliminating,
title={Eliminating dependent pattern matching},
author={Goguen, Healfdene and McBride, Conor and McKinna, James},
journal={Algebra, Meaning, and Computation},
pages={521--540},
year={2006},
publisher={Springer Berlin/Heidelberg}
}
@article{church1940formulation,
title={A formulation of the simple theory of types},
author={Church, Alonzo},
journal={The journal of symbolic logic},
volume={5},
number={02},
pages={56--68},
year={1940},
publisher={Cambridge Univ Press}
}
@book{girard1989proofs,
title={Proofs and types},
author={Girard, Jean-Yves and Taylor, Paul and Lafont, Yves},
volume={7},
year={1989},
publisher={Cambridge University Press Cambridge}
}
@inproceedings{bernardy2010parametricity,
title={Parametricity and dependent types},
author={Bernardy, Jean-Philippe and Jansson, Patrik and Paterson, Ross},
booktitle={ACM Sigplan Notices},
volume={45},
number={9},
pages={345--356},
year={2010},
organization={ACM}
}
@String{j-jucs = "Journal of Universal Computer Science"}
@Article{niels,
author = "Henning Basold and Herman Geuvers and Niels van der Weide",
title = "Higher Inductive Types in Programming",
abstract = "We propose general rules for higher inductive types with non-dependent and dependent elimination rules. These can be used to give a formal treatment of data types with laws as has been discussed by David Turner in his earliest papers on Miranda [Turner(1985)]. The non-dependent elimination scheme is particularly useful for defining functions by recursion and pattern matching, while the dependent elimination scheme gives an induction proof principle. We have rules for non-recursive higher inductive types, like the integers, but also for recursive higher inductive types like the truncation. In the present paper we only allow path constructors (so there are no higher path constructors), which is sufficient for treating various interesting examples from functional programming, as we will briefly show in the paper: arithmetic modulo, integers and finite sets.",
journal = j-jucs,
year = "2017",
volume = "23",
number = "1",
pages = "63--88",
date = "2017-01-28",
month = "jan"}
@article{chapman2010gentle,
title={The gentle art of levitation},
author={Chapman, James and Dagand, Pierre-{\'E}variste and McBride, Conor and Morris, Peter},
journal={ACM Sigplan Notices},
volume={45},
number={9},
pages={3--14},
year={2010},
publisher={ACM}
}
@inproceedings{next700,
author = {Boulier, Simon and P{\'e}drot, Pierre-Marie and Tabareau, Nicolas},
title = {The Next 700 Syntactical Models of Type Theory},
booktitle = {Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs},
series = {CPP 2017},
year = {2017},
isbn = {978-1-4503-4705-1},
location = {Paris, France},
pages = {182--194},
numpages = {13},
doi = {10.1145/3018610.3018620},
acmid = {3018620},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {Dependent type theory, Program translation},
}
@MastersThesis{nielsmsc,
author = {Niels van der Weide},
title = {Higher Inductive Types},
school = {Radboud University, Nijmegen},
year = {2016}}
@InProceedings{gabe,
author="Altenkirch, Thorsten
and Capriotti, Paolo
and Dijkstra, Gabe
and Kraus, Nicolai
and Nordvall Forsberg, Fredrik",
editor="Baier, Christel
and Dal Lago, Ugo",
title="Quotient Inductive-Inductive Types",
booktitle="Foundations of Software Science and Computation Structures",
year="2018",
publisher="Springer International Publishing",
address="Cham",
pages="293--310",
abstract="Higher inductive types (HITs) in Homotopy Type Theory allow the definition of datatypes which have constructors for equalities over the defined type. HITs generalise quotient types, and allow to define types with non-trivial higher equality types, such as spheres, suspensions and the torus. However, there are also interesting uses of HITs to define types satisfying uniqueness of equality proofs, such as the Cauchy reals, the partiality monad, and the well-typed syntax of type theory. In each of these examples we define several types that depend on each other mutually, i.e. they are inductive-inductive definitions. We call those HITs quotient inductive-inductive types (QIITs). Although there has been recent progress on a general theory of HITs, there is not yet a theoretical foundation for the combination of equality constructors and induction-induction, despite many interesting applications. In the present paper we present a first step towards a semantic definition of QIITs. In particular, we give an initial-algebra semantics. We further derive a section induction principle, stating that every algebra morphism into the algebra in question has a section, which is close to the intuitively expected elimination rules.",
isbn="978-3-319-89366-2"
}
@inproceedings{krausprop,
author = {Kraus, Nicolai},
title = {Constructions with Non-Recursive Higher Inductive Types},
booktitle = {Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science},
series = {LICS '16},
year = {2016},
isbn = {978-1-4503-4391-6},
location = {New York, NY, USA},
pages = {595--604},
numpages = {10},
doi = {10.1145/2933575.2933586},
acmid = {2933586},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {higher inductive types, homotopy type theory, sequential colimits, truncation elimination, van Doorn construction},
}
@inproceedings{doorn,
author = {Doorn, Floris van},
title = {Constructing the Propositional Truncation Using Non-recursive HITs},
booktitle = {Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs},
series = {CPP 2016},
year = {2016},
isbn = {978-1-4503-4127-1},
location = {St. Petersburg, FL, USA},
pages = {122--129},
numpages = {8},
doi = {10.1145/2854065.2854076},
acmid = {2854076},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {Higher Inductive Types, Homotopy Type Theory, Lean, Propositional Truncation},
}
@MISC{formalQIIT,
author = {Ambrus Kaposi and Andr{\'a}s Kov{\'a}cs},
title = {Agda formalisation for the paper {``Codes for Quotient Inductive Inductive Types''}},
note = {Available online at the first author's website},
year = {2017}}
@inproceedings{henning,
title = {Type {{Theory}} Based on {{Dependent Inductive}} and {{Coinductive Types}}},
doi = {10.1145/2933575.2934514},
booktitle = {Proceedings of {{LICS}} '16},
publisher = {{ACM}},
author = {Basold, Henning and Geuvers, Herman},
editor = {Grohe, Martin and Koskinen, Eric and Shankar, Natarajan},
year = {2016},
keywords = {own},
pages = {327--336}
}
@PHDTHESIS{kaposi-phd,
author = {Ambrus Kaposi},
title = {Type theory in a type theory with quotient inductive types},
school = {University of Nottingham},
year = {2017}}
@Unpublished{hts,
author = {Vladimir Voevodsky},
title = {A simple type system with two identity types},
note = {Unpublished note},
year = 2013}
@article{semisegal,
author = {Capriotti, Paolo and Kraus, Nicolai},
title = {Univalent Higher Categories via Complete Semi-Segal Types},
journal = {Proc. ACM Program. Lang.},
issue_date = {January 2018},
volume = {2},
number = {POPL},
month = dec,
year = {2017},
issn = {2475-1421},
pages = {44:1--44:29},
articleno = {44},
numpages = {29},
doi = {10.1145/3158132},
acmid = {3158132},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {Homotopy type theory, complete Segal spaces, higher categories},
}
@article{moeneclaey,
title = "Finitary Higher Inductive Types in the Groupoid Model",
journal = "Electronic Notes in Theoretical Computer Science",
volume = "336",
pages = "119 - 134",
year = "2018",
note = "The Thirty-third Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIII)",
issn = "1571-0661",
doi = {10.1016/j.entcs.2018.03.019},
author = "Peter Dybjer and Hugo Moeneclaey",
keywords = "intuitionistic type theory, identity types, homotopy type theory, higher inductive types, setoids, groupoids"
}
@article{displayedcats,
TITLE = {{Displayed Categories}},
AUTHOR = {Ahrens, Benedikt and Lumsdaine, Peter LeFanu},
URL = {https://lmcs.episciences.org/5252},
DOI = {10.23638/LMCS-15(1:20)2019},
JOURNAL = {{Logical Methods in Computer Science}},
VOLUME = {{Volume 15, Issue 1}},
YEAR = {2019},
MONTH = Mar,
KEYWORDS = {Mathematics - Category Theory ; Mathematics - Logic ; 18A15, 03B15, 03B70 ; F.4.1},
}
@InProceedings{hiit,
author = {Ambrus Kaposi and Andr{\'a}s Kov{\'a}cs},
title = {{A Syntax for Higher Inductive-Inductive Types}},
booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
pages = {20:1--20:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-077-4},
ISSN = {1868-8969},
year = {2018},
volume = {108},
editor = {H{\'e}l{\`e}ne Kirchner},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2018/9190},
URN = {urn:nbn:de:0030-drops-91906},
doi = {10.4230/LIPIcs.FSCD.2018.20},
annote = {Keywords: homotopy type theory, inductive-inductive types, higher inductive types, quotient inductive types, logical relations}
}
@article{cubicalhits,
author = {Coquand, Thierry and Huber, Simon and M\"ortberg, Anders},
journal = {LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science},
year = {2018},
isbn = {978-1-4503-5583-4},
location = {Oxford, United Kingdom},
publisher = {ACM},
title = {On Higher Inductive Types in Cubical Type Theory}
}
@article{kaposi2019constructing,
title={Constructing quotient inductive-inductive types},
author={Kaposi, Ambrus and Kov{\'a}cs, Andr{\'a}s and Altenkirch, Thorsten},
journal={Proceedings of the ACM on Programming Languages},
volume={3},
number={POPL},
pages={2},
year={2019},
publisher={ACM}
}
@article{ahrens2015univalent,
title={Univalent categories and the Rezk completion},
author={Ahrens, Benedikt and Kapulkin, Krzysztof and Shulman, Michael},
journal={Mathematical Structures in Computer Science},
volume={25},
number={5},
pages={1010--1039},
year={2015},
publisher={Cambridge University Press}
}
@inproceedings{winterhalter2019eliminating,
title={Eliminating reflection from type theory},
author={Winterhalter, Th{\'e}o and Sozeau, Matthieu and Tabareau, Nicolas},
booktitle={Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs},
pages={91--103},
year={2019},
organization={ACM}
}
@book{streicher2012semantics,
title={Semantics of type theory: correctness, completeness and independence results},
author={Streicher, Thomas},
year={2012},
publisher={Springer Science \& Business Media}
}
@article{abel2017decidability,
title={Decidability of conversion for type theory in type theory},
author={Abel, Andreas and {\"O}hman, Joakim and Vezzosi, Andrea},
journal={Proceedings of the ACM on Programming Languages},
volume={2},
number={POPL},
pages={23},
year={2017},
publisher={ACM}
}
@article{altenkirch2018towards,
title={Towards the syntax and semantics of higher dimensional type theory},
author={Altenkirch, Thorsten and Kraus, Nicolai},
year={2018}
}
@article{finster2019structure,
title={Structure and Equality in Type Systems},
author={Finster, Eric},
year={2019}
}
@phdthesis{nuyts2015towards,
title={Towards a directed homotopy type theory based on 4 kinds of variance},
author={Nuyts, Andreas},
year={2015},
school={MA thesis. KU Leuven}
}
@article{riehl2017type,
title={A type theory for synthetic $\infty$-categories},
author={Riehl, Emily and Shulman, Michael},
journal={arXiv preprint arXiv:1705.07442},
year={2017}
}
@article{pinyo2018integers,
title={Integers as a Higher Inductive Type},
author={Pinyo, Gun and Altenkirch, Thorsten},
journal={TYPES 2018},
year={2018}
}
@misc{cavallointegers,
author = {Cavallo, Evan and M\"ortberg, Anders},
title = {Successor on biinv-int which cancels pred exactly},
year = {2018 (accessed 2019-02-04)},
howpublished = "\url{https://github.com/RedPRL/redtt/blob/master/library/cool/biinv-int.red}"
}
@article{cockx2016sprinkles,
title={Sprinkles of extensionality for your vanilla type theory},
author={Cockx, Jesper and Abel, Andreas},
journal={TYPES 2016},
year={2016}
}
@article{coquandnorm,
author = {Thierry Coquand},
title = {Canonicity and normalization for dependent type theory},
journal = {Theor. Comput. Sci.},
volume = {777},
pages = {184--191},
year = {2019},
url = {https://doi.org/10.1016/j.tcs.2019.01.015},
doi = {10.1016/j.tcs.2019.01.015},
timestamp = {Wed, 03 Jul 2019 14:50:25 +0200},
biburl = {https://dblp.org/rec/journals/tcs/Coquand19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{gluing,
author = {Ambrus Kaposi and Simon Huber and Christian Sattler},
year = {2019},
title = {Gluing for type theory},
booktitle = {Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
editor = {Geuvers, Herman},
}
@inproceedings{homotopycanonicity,
author = {Thierry Coquand and Simon Huber and Christian Sattler},
year = {2019},
title = {Homotopy canonicity for cubical type theory},
booktitle = {Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
editor = {Geuvers, Herman},
}
@inproceedings{Wieczorek:2018:CFN:3176245.3167091,
author = {Wieczorek, Pawe\l and Biernacki, Dariusz},
title = {A {C}oq Formalization of Normalization by Evaluation for {M}artin-{L}\"{o}f Type Theory},
booktitle = {Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs},
series = {CPP 2018},
year = {2018},
isbn = {978-1-4503-5586-5},
location = {Los Angeles, CA, USA},
pages = {266--279},
numpages = {14},
url = {http://doi.acm.org/10.1145/3167091},
doi = {10.1145/3167091},
acmid = {3167091},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {Coq, normalization by evaluation, program certification, type theory},
}
@article{lmcs:4005,
TITLE = {{Normalisation by Evaluation for Type Theory, in Type Theory}},
AUTHOR = {Altenkirch, Thorsten and Kaposi, Ambrus},
URL = {https://lmcs.episciences.org/4005},
DOI = {10.23638/LMCS-13(4:1)2017},
JOURNAL = {{Logical Methods in Computer Science}},
VOLUME = {{Volume 13, Issue 4}},
YEAR = {2017},
MONTH = Oct,
KEYWORDS = {Computer Science - Logic in Computer Science ; F.4.1},
}
@inproceedings{DBLP:conf/itp/AnandBCST18,
author = {Abhishek Anand and
Simon Boulier and
Cyril Cohen and
Matthieu Sozeau and
Nicolas Tabareau},
title = {Towards Certified Meta-Programming with Typed Template-Coq},
booktitle = {Interactive Theorem Proving - 9th International Conference, {ITP}
2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
UK, July 9-12, 2018, Proceedings},
pages = {20--39},
year = {2018},
crossref = {DBLP:conf/itp/2018},
url = {https://doi.org/10.1007/978-3-319-94821-8\_2},
doi = {10.1007/978-3-319-94821-8\_2},
timestamp = {Wed, 03 Oct 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/bib/conf/itp/AnandBCST18},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/itp/2018,
editor = {Jeremy Avigad and
Assia Mahboubi},
title = {Interactive Theorem Proving - 9th International Conference, {ITP}
2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
UK, July 9-12, 2018, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10895},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-94821-8},
doi = {10.1007/978-3-319-94821-8},
isbn = {978-3-319-94820-1},
timestamp = {Thu, 05 Jul 2018 14:28:25 +0200},
biburl = {https://dblp.org/rec/bib/conf/itp/2018},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{Pfenning:1988:HAS:960116.54010,
author = {Pfenning, F. and Elliott, C.},
title = {Higher-order Abstract Syntax},
journal = {SIGPLAN Not.},
issue_date = {July 1988},
volume = {23},
number = {7},
month = jun,
year = {1988},
issn = {0362-1340},
pages = {199--208},
numpages = {10},
url = {http://doi.acm.org/10.1145/960116.54010},
doi = {10.1145/960116.54010},
acmid = {54010},
publisher = {ACM},
address = {New York, NY, USA},
}
@inproceedings{Hofmann:1999:SAH:788021.788940,
author = {Hofmann, Martin},
title = {Semantical Analysis of Higher-Order Abstract Syntax},
booktitle = {Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science},
series = {LICS '99},
year = {1999},
isbn = {0-7695-0158-3},
pages = {204--},
url = {http://dl.acm.org/citation.cfm?id=788021.788940},
acmid = {788940},
publisher = {IEEE Computer Society},
address = {Washington, DC, USA},
}
@techreport{despeyroux:inria-00074124,
TITLE = {{Higher-Order Abstract Syntax in Coq}},
AUTHOR = {Despeyroux, Jo{\"e}lle and Felty, Amy and Hirschowitz, Andr{\'e}},
URL = {https://hal.inria.fr/inria-00074124},
NUMBER = {RR-2556},
INSTITUTION = {{INRIA}},
YEAR = {1995},
MONTH = May,
KEYWORDS = {TYPE THEORY ; THEOREM PROVING ; LOGICAL FRAMEWORK ; HIGHER-ORDER ABSTRACT SYNTAX ; COQ},
PDF = {https://hal.inria.fr/inria-00074124/file/RR-2556.pdf},
HAL_ID = {inria-00074124},
HAL_VERSION = {v1},
}
@inproceedings{Chlipala:2008:PHA:1411204.1411226,
author = {Chlipala, Adam},
title = {Parametric Higher-order Abstract Syntax for Mechanized Semantics},
booktitle = {Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming},
series = {ICFP '08},
year = {2008},
isbn = {978-1-59593-919-7},
location = {Victoria, BC, Canada},
pages = {143--156},
numpages = {14},
url = {http://doi.acm.org/10.1145/1411204.1411226},
doi = {10.1145/1411204.1411226},
acmid = {1411226},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {compiler verification, dependent types, interactive proof assistants, type-theoretic semantics},
}
@article{tabareau:hal-01559073,
TITLE = {{Equivalences for Free}},
AUTHOR = {Tabareau, Nicolas and Tanter, {\'E}ric and Sozeau, Matthieu},
URL = {https://hal.inria.fr/hal-01559073},
JOURNAL = {{Proceedings of the ACM on Programming Languages}},
HAL_LOCAL_REFERENCE = {ACL+},
HAL_LOCAL_REFERENCE = {BEST},
PUBLISHER = {{ACM}},
SERIES = {ICFP'18},
PAGES = {1-29},
YEAR = {2018},
MONTH = Sep,
DOI = {10.1145/3234615},
KEYWORDS = {Coq ; Type theory ; Homotopy Type Theory ; Parametricity ; Type structures ; Program reasoning},
PDF = {https://hal.inria.fr/hal-01559073/file/main_icfp.pdf},
HAL_ID = {hal-01559073},
HAL_VERSION = {v5},
}
@inproceedings{Hou(Favonia):2016:MBC:2933575.2934545,
author = {Hou (Favonia), Kuen-Bang and Finster, Eric and Licata, Daniel R. and Lumsdaine, Peter LeFanu},
title = {A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory},
booktitle = {Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science},
series = {LICS '16},
year = {2016},
isbn = {978-1-4503-4391-6},
location = {New York, NY, USA},
pages = {565--574},
numpages = {10},
url = {http://doi.acm.org/10.1145/2933575.2934545},
doi = {10.1145/2933575.2934545},
acmid = {2934545},
publisher = {ACM},
address = {New York, NY, USA},
}
@InProceedings{orton_et_al:LIPIcs:2016:6564,
author = {Ian Orton and Andrew M. Pitts},
title = {{Axioms for Modelling Cubical Type Theory in a Topos}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {24:1--24:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Jean-Marc Talbot and Laurent Regnier},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2016/6564},
URN = {urn:nbn:de:0030-drops-65647},
doi = {10.4230/LIPIcs.CSL.2016.24},
annote = {Keywords: models of dependent type theory, homotopy type theory, cubical sets, cubical type theory, topos, univalence}
}
@Misc{formalisation,
author = {Ambrus Kaposi and Andr{\'a}s Kov{\'a}cs and Nicolai Kraus},
title = {Formalisations in {A}gda using a morally correct shallow embedding},
url = {https://bitbucket.org/akaposi/shallow/src/master/},
month = {May},
year = {2019}
}
@Manual{Coq,
title = {The Coq proof assistant reference manual},
author = {\mbox{The Coq development team}},
organization = {LogiCal Project},
note = {Version 8.9},
year = {2019},
url = "http://coq.inria.fr"
}
@inproceedings{leanprover,
title={The Lean theorem prover (system description)},
author={de Moura, Leonardo and Kong, Soonho and Avigad, Jeremy and Van Doorn, Floris and von Raumer, Jakob},
booktitle={International Conference on Automated Deduction},
pages={378--388},
year={2015},
organization={Springer}
}
@article{coquand2018canonicity,
title={Canonicity and normalisation for Dependent Type Theory},
author={Coquand, Thierry},
journal={arXiv preprint arXiv:1810.09367},
year={2018}
}
@phdthesis{huber-thesis,
author = {Huber, Simon},
title = {Cubical Interpretations of Type Theory},
school = {University of Gothenburg},
year = {2016}}
@phdthesis{diehl-thesis,
title={Fully Generic Programming over Closed Universes of Inductive-Recursive Types},
author={Diehl, Larry},
year={2017},
school={Portland State University}
}
@inproceedings{birkedal2011first,
title={First steps in synthetic guarded domain theory: step-indexing in the topos of trees},
author={Birkedal, Lars and Mogelberg, Rasmus Ejlers and Schwinghammer, Jan and Stovring, Kristian},
booktitle={2011 IEEE 26th Annual Symposium on Logic in Computer Science},
pages={55--64},
year={2011},
organization={IEEE}
}
@article{clairambault2014biequivalence,
title={The biequivalence of locally cartesian closed categories and Martin-L{\"o}f type theories},
author={Clairambault, Pierre and Dybjer, Peter},
journal={Mathematical Structures in Computer Science},
volume={24},
number={6},
year={2014},
publisher={Cambridge University Press}
}
@article{sterling2019algebraic,
author = {Jonathan Sterling},
title = {Algebraic Type Theory and Universe Hierarchies},
journal = {CoRR},
volume = {abs/1902.08848},
year = {2019},
url = {http://arxiv.org/abs/1902.08848},
archivePrefix = {arXiv},
eprint = {1902.08848},
timestamp = {Tue, 21 May 2019 18:03:38 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1902-08848.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{carette2007finally,
title={Finally tagless, partially evaluated},
author={Carette, Jacques and Kiselyov, Oleg and Shan, Chung-Chieh},
booktitle={Asian Symposium on Programming Languages and Systems},
pages={222--238},
year={2007},
organization={Springer}
}
@article{dependentrightadjoints,
author = {Lars Birkedal and
Ranald Clouston and
Bassel Mannaa and
Rasmus Ejlers M{\o}gelberg and
Andrew M. Pitts and
Bas Spitters},
title = {Modal dependent type theory and dependent right adjoints},
journal = {Math. Struct. Comput. Sci.},
volume = {30},
number = {2},
pages = {118--138},
year = {2020},
url = {https://doi.org/10.1017/S0960129519000197},
doi = {10.1017/S0960129519000197},
timestamp = {Wed, 01 Apr 2020 08:48:46 +0200},
biburl = {https://dblp.org/rec/journals/mscs/BirkedalCMMPS20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{jacobs1993comprehension,
title={Comprehension categories and the semantics of type dependency},
author={Jacobs, Bart},
journal={Theoretical Computer Science},
volume={107},
number={2},
pages={169--207},
year={1993},
publisher={Elsevier}
}
@phdthesis{dijkstra2017quotient,
title={Quotient inductive-inductive definitions},
author={Dijkstra, Gabe},
year={2017},
school={University of Nottingham}
}
@article{cohen2016cubical,
title={Cubical type theory: a constructive interpretation of the univalence axiom},
author={Cohen, Cyril and Coquand, Thierry and Huber, Simon and M{\"o}rtberg, Anders},
journal={arXiv preprint arXiv:1611.02108},
year={2016}
}
@article{angiuli2016computational,
title={Computational higher type theory I: Abstract cubical realizability},
author={Angiuli, Carlo and Harper, Robert and Wilson, Todd},
journal={arXiv preprint arXiv:1604.08873},
year={2016}
}
@article{angiuli2018cartesian,
title={Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities},
author={Angiuli, Carlo and Hou, Kuen-Bang Favonia and Harper, Robert},
journal={Computer Science Logic 2018},
year={2018}
}
@book{johnstone2002sketches,
title={Sketches of an elephant: A topos theory compendium},
author={Johnstone, Peter T},
volume={2},
year={2002},
publisher={Oxford University Press}
}
@article{10.1145/3290314,
author = {Cavallo, Evan and Harper, Robert},
title = {Higher Inductive Types in Cubical Computational Type Theory},
year = {2019},
issue_date = {January 2019},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {3},
number = {POPL},
url = {https://doi.org/10.1145/3290314},
doi = {10.1145/3290314},
journal = {Proc. ACM Program. Lang.},
month = jan,
articleno = {Article 1},
numpages = {27},
keywords = {cubical type theory, higher inductive types, homotopy type theory}
}
@inproceedings{10.1145/3209108.3209130,
author = {Awodey, Steve and Frey, Jonas and Speight, Sam},
title = {Impredicative Encodings of (Higher) Inductive Types},
year = {2018},
isbn = {9781450355834},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3209108.3209130},
doi = {10.1145/3209108.3209130},
booktitle = {Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science},
pages = {76–85},
numpages = {10},
keywords = {System F, Impredicativity, Higher inductive types, Impredicative encodings, Homotopy type theory, Martin-L\"{o}f type theory, Inductive types},
location = {Oxford, United Kingdom},
series = {LICS ’18}
}
@InProceedings{jasper,
author="Hugunin, Jasper",
editor="Boja{\'{n}}czyk, Miko{\l}aj
and Simpson, Alex",
title="Constructing Inductive-Inductive Types in Cubical Type Theory",
booktitle="Foundations of Software Science and Computation Structures",
year="2019",
publisher="Springer International Publishing",
address="Cham",
pages="295--312",
abstract="Inductive-inductive types are a joint generalization of mutual inductive types and indexed inductive types. In extensional type theory, inductive-inductive types can be constructed from inductive types, and this construction has been conjectured to work in intensional type theory as well. In this paper, we show that the existing construction requires Uniqueness of Identity Proofs, and present a new construction (which we conjecture generalizes) of one particular inductive-inductive type in cubical type theory, which is compatible with homotopy type theory.",
isbn="978-3-030-17127-8"
}
@article{induction-is-enough,
author = {Kaposi, Ambrus and Kovács, András and Lafont Ambroise},
title = {For Induction-Induction, Induction is Enough},
year = {2019},
journal = {Submitted to TYPES 2019 post-proceedings}
}
@Unpublished{brunerie,
author = {Guillaume Brunerie},
title = {A formalization of the initiality conjecture in Agda},
note = {Slides of a talk at the Homotopy Type Theory 2019 Conference, Carnegie Mellon University, Pittsburgh, Pennsylvania},
month = {August},
year = {2019},
url = {https://guillaumebrunerie.github.io/pdf/initiality.pdf},
}
@article{voevodsky2011resizing,
title={Resizing rules, slides from a talk at TYPES2011},
author={Voevodsky, Vladimir},
journal={At author’s webpage},
year={2011}
}
@inproceedings{partiality,
author = {Altenkirch, Thorsten and Danielsson, Nils Anders and Kraus, Nicolai},
title = {Partiality, Revisited},
year = {2017},
isbn = {9783662544570},
publisher = {Springer-Verlag},
address = {Berlin, Heidelberg},
url = {https://doi.org/10.1007/978-3-662-54458-7_31},
doi = {10.1007/978-3-662-54458-7_31},
booktitle = {Proceedings of the 20th International Conference on Foundations of Software Science and Computation Structures - Volume 10203},
pages = {534–549},
numpages = {16}
}
@article{vezzosicubical,
title={Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types},
author={Vezzosi, Andrea and M{\"o}rtberg23, Anders and Abel, Andreas}
}
@article{nanevski2008contextual,
author = {Aleksandar Nanevski and
Frank Pfenning and
Brigitte Pientka},
title = {Contextual modal type theory},
journal = {{ACM} Trans. Comput. Log.},
volume = {9},
number = {3},
pages = {23:1--23:49},
year = {2008},
url = {https://doi.org/10.1145/1352582.1352591},
doi = {10.1145/1352582.1352591},
timestamp = {Tue, 06 Nov 2018 12:51:53 +0100},
biburl = {https://dblp.org/rec/journals/tocl/NanevskiPP08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@phdthesis{gundry2013type,
author = {Adam Michael Gundry},
title = {Type inference, Haskell and dependent types},
school = {University of Strathclyde, Glasgow, {UK}},
year = {2013},
url = {http://oleg.lib.strath.ac.uk/R/?func=dbin-jump-full\&object\_id=22728},
timestamp = {Mon, 18 Jun 2018 17:33:10 +0200},
biburl = {https://dblp.org/rec/phd/ethos/Gundry13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{dunfield2013complete,
author = {Joshua Dunfield and
Neelakantan R. Krishnaswami},
editor = {Greg Morrisett and
Tarmo Uustalu},
title = {Complete and easy bidirectional typechecking for higher-rank polymorphism},
booktitle = {{ACM} {SIGPLAN} International Conference on Functional Programming,
ICFP'13, Boston, MA, {USA} - September 25 - 27, 2013},
pages = {429--442},
publisher = {{ACM}},
year = {2013},
url = {https://doi.org/10.1145/2500365.2500582},
doi = {10.1145/2500365.2500582},
timestamp = {Tue, 06 Nov 2018 16:59:24 +0100},
biburl = {https://dblp.org/rec/conf/icfp/DunfieldK13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{eisenberg2016dependent,
author = {Richard A. Eisenberg},
title = {Dependent Types in Haskell: Theory and Practice},
journal = {CoRR},
volume = {abs/1610.07978},
year = {2016},
url = {http://arxiv.org/abs/1610.07978},
archivePrefix = {arXiv},
eprint = {1610.07978},
timestamp = {Mon, 13 Aug 2018 16:47:17 +0200},
biburl = {https://dblp.org/rec/journals/corr/Eisenberg16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@mastersthesis{johansson2015eliminating,
title={Eliminating the problems of hidden-lambda insertion-Restricting implicit arguments for increased predictability of type checking in a functional programming language with depending types},
author={Johansson, Marcus and Lloyd, Jesper},
school={Chalmers University of Technology},
year={2015}
}
@inproceedings{licata2018internal,
author = {Daniel R. Licata and
Ian Orton and
Andrew M. Pitts and
Bas Spitters},
editor = {H{\'{e}}l{\`{e}}ne Kirchner},
title = {Internal Universes in Models of Homotopy Type Theory},
booktitle = {3rd International Conference on Formal Structures for Computation
and Deduction, {FSCD} 2018, July 9-12, 2018, Oxford, {UK}},
series = {LIPIcs},
volume = {108},
pages = {22:1--22:17},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2018},
url = {https://doi.org/10.4230/LIPIcs.FSCD.2018.22},
doi = {10.4230/LIPIcs.FSCD.2018.22},
timestamp = {Tue, 11 Feb 2020 15:52:14 +0100},
biburl = {https://dblp.org/rec/conf/rta/LicataOPS18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{leijen2008hmf,
author = {Daan Leijen},
editor = {James Hook and
Peter Thiemann},
title = {{HMF:} simple type inference for first-class polymorphism},
booktitle = {Proceeding of the 13th {ACM} {SIGPLAN} international conference on
Functional programming, {ICFP} 2008, Victoria, BC, Canada, September
20-28, 2008},
pages = {283--294},
publisher = {{ACM}},
year = {2008},
url = {https://doi.org/10.1145/1411204.1411245},
doi = {10.1145/1411204.1411245},
timestamp = {Mon, 23 Mar 2020 12:22:51 +0100},
biburl = {https://dblp.org/rec/conf/icfp/Leijen08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{leijen2009flexible,
author = {Daan Leijen},
editor = {Zhong Shao and
Benjamin C. Pierce},
title = {Flexible types: robust type inference for first-class polymorphism},
booktitle = {Proceedings of the 36th {ACM} {SIGPLAN-SIGACT} Symposium on Principles
of Programming Languages, {POPL} 2009, Savannah, GA, USA, January
21-23, 2009},
pages = {66--77},
publisher = {{ACM}},
year = {2009},
url = {https://doi.org/10.1145/1480881.1480891},
doi = {10.1145/1480881.1480891},
timestamp = {Tue, 06 Nov 2018 11:07:44 +0100},
biburl = {https://dblp.org/rec/conf/popl/Leijen09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{serrano2018guarded,
author = {Alejandro Serrano and
Jurriaan Hage and
Dimitrios Vytiniotis and
Simon {Peyton Jones}},
editor = {Jeffrey S. Foster and
Dan Grossman},
title = {Guarded impredicative polymorphism},
booktitle = {Proceedings of the 39th {ACM} {SIGPLAN} Conference on Programming
Language Design and Implementation, {PLDI} 2018, Philadelphia, PA,
USA, June 18-22, 2018},
pages = {783--796},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3192366.3192389},
doi = {10.1145/3192366.3192389},
timestamp = {Tue, 19 Feb 2019 13:37:49 +0100},
biburl = {https://dblp.org/rec/conf/pldi/SerranoHVJ18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{vytiniotis2006boxy,
author = {Dimitrios Vytiniotis and
Stephanie Weirich and
Simon L. {Peyton Jones}},
editor = {John H. Reppy and
Julia L. Lawall},
title = {Boxy types: inference for higher-rank types and impredicativity},
booktitle = {Proceedings of the 11th {ACM} {SIGPLAN} International Conference on
Functional Programming, {ICFP} 2006, Portland, Oregon, USA, September
16-21, 2006},
pages = {251--262},
publisher = {{ACM}},
year = {2006},
url = {https://doi.org/10.1145/1159803.1159838},
doi = {10.1145/1159803.1159838},
timestamp = {Sat, 19 Oct 2019 20:03:54 +0200},
biburl = {https://dblp.org/rec/conf/icfp/VytiniotisWJ06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{abel2011higher,
author = {Andreas Abel and
Brigitte Pientka},
editor = {C.{-}H. Luke Ong},
title = {Higher-Order Dynamic Pattern Unification for Dependent Types and Records},
booktitle = {Typed Lambda Calculi and Applications - 10th International Conference,
{TLCA} 2011, Novi Sad, Serbia, June 1-3, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6690},
pages = {10--26},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-21691-6\_5},
doi = {10.1007/978-3-642-21691-6\_5},
timestamp = {Tue, 14 May 2019 10:00:41 +0200},
biburl = {https://dblp.org/rec/conf/tlca/AbelP11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{vytiniotis2008fph,
author = {Dimitrios Vytiniotis and
Stephanie Weirich and
Simon L. {Peyton Jones}},
editor = {James Hook and
Peter Thiemann},
title = {{FPH:} first-class polymorphism for Haskell},
booktitle = {Proceeding of the 13th {ACM} {SIGPLAN} international conference on
Functional programming, {ICFP} 2008, Victoria, BC, Canada, September
20-28, 2008},
pages = {295--306},
publisher = {{ACM}},
year = {2008},
url = {https://doi.org/10.1145/1411204.1411246},
doi = {10.1145/1411204.1411246},
timestamp = {Mon, 23 Mar 2020 12:22:51 +0100},
biburl = {https://dblp.org/rec/conf/icfp/VytiniotisWJ08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@Unpublished{serrano2020a,
author = {Serrano, Alejandro and Hage, Jurriaan and Peyton Jones, Simon and Vytiniotis, Dimitrios},
title = {A quick look at impredicativity},
year = {2020},
month = {January},
abstract = {Type inference for parametric polymorphism is wildly successful, but has always suffered from an embarrassing flaw: polymorphic types are themselves not first class. We present Quick Look, a practical, implemented, and deployable design for impredicative type inference. To demonstrate our claims, we have modified GHC, a production-quality Haskell compiler, to support impredicativity. The changes required are modest, localised, and are fully compatible with GHC's myriad other type system extensions.},
url = {https://www.microsoft.com/en-us/research/publication/a-quick-look-at-impredicativity/},
note = {In submission},
}
@article{vytiniotis2011outsidein,
author = {Dimitrios Vytiniotis and
Simon L. {Peyton Jones} and
Tom Schrijvers and
Martin Sulzmann},
title = {OutsideIn(X) Modular type inference with local assumptions},
journal = {J. Funct. Program.},
volume = {21},
number = {4-5},
pages = {333--412},
year = {2011},
url = {https://doi.org/10.1017/S0956796811000098},
doi = {10.1017/S0956796811000098},
timestamp = {Fri, 30 Nov 2018 13:26:43 +0100},
biburl = {https://dblp.org/rec/journals/jfp/VytiniotisJSS11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{coquand1996algorithm,
author = {Thierry Coquand},
title = {An Algorithm for Type-Checking Dependent Types},
journal = {Sci. Comput. Program.},
volume = {26},
number = {1-3},
pages = {167--177},
year = {1996},
url = {https://doi.org/10.1016/0167-6423(95)00021-6},
doi = {10.1016/0167-6423(95)00021-6},
timestamp = {Sat, 27 May 2017 14:22:56 +0200},
biburl = {https://dblp.org/rec/journals/scp/Coquand96.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{le2014mlf,
author = {Didier Le Botlan and
Didier R{\'{e}}my},
title = {ML\({}^{\mbox{F}}\): raising {ML} to the power of system {F}},
journal = {{SIGPLAN} Notices},
volume = {38},
number = {9},
pages = {27--38},
year = {2003},
url = {https://doi.org/10.1145/944746.944709},
doi = {10.1145/944746.944709},
timestamp = {Tue, 06 Nov 2018 12:51:13 +0100},
biburl = {https://dblp.org/rec/journals/sigplan/BotlanR03.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{remy2007graphical,
title={A graphical presentation of MLF types with a linear-time unification algorithm},
author={R{\'e}my, Didier and Yakobowski, Boris},
booktitle={Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation},
pages={27--38},
year={2007}
}
@inproceedings{vytiniotis2010let,
title={Let should not be generalized},
author={Vytiniotis, Dimitrios and Peyton Jones, Simon and Schrijvers, Tom},
booktitle={Proceedings of the 5th ACM SIGPLAN workshop on Types in language design and implementation},
pages={39--50},
year={2010}
}
@inproceedings{eisenberg2016visible,
author = {Richard A. Eisenberg and
Stephanie Weirich and
Hamidhasan G. Ahmed},
editor = {Peter Thiemann},
title = {Visible Type Application},
booktitle = {Programming Languages and Systems - 25th European Symposium on Programming,
{ESOP} 2016, Held as Part of the European Joint Conferences on Theory
and Practice of Software, {ETAPS} 2016, Eindhoven, The Netherlands,
April 2-8, 2016, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9632},
pages = {229--254},
publisher = {Springer},
year = {2016},
url = {https://doi.org/10.1007/978-3-662-49498-1\_10},
doi = {10.1007/978-3-662-49498-1\_10},
timestamp = {Mon, 23 Mar 2020 12:22:51 +0100},
biburl = {https://dblp.org/rec/conf/esop/EisenbergWA16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{kaposi2019gluing,
author = {Ambrus Kaposi and
Simon Huber and
Christian Sattler},
editor = {Herman Geuvers},
title = {Gluing for Type Theory},
booktitle = {4th International Conference on Formal Structures for Computation
and Deduction, {FSCD} 2019, June 24-30, 2019, Dortmund, Germany},
series = {LIPIcs},
volume = {131},
pages = {25:1--25:19},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2019},
url = {https://doi.org/10.4230/LIPIcs.FSCD.2019.25},
doi = {10.4230/LIPIcs.FSCD.2019.25},
timestamp = {Tue, 11 Feb 2020 15:52:14 +0100},
biburl = {https://dblp.org/rec/conf/rta/KaposiHS19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{decidableconv,
author = {Andreas Abel and
Joakim {\"{O}}hman and
Andrea Vezzosi},
title = {Decidability of conversion for type theory in type theory},
journal = {Proc. {ACM} Program. Lang.},
volume = {2},
number = {{POPL}},
pages = {23:1--23:29},
year = {2018},
url = {https://doi.org/10.1145/3158111},
doi = {10.1145/3158111},
timestamp = {Thu, 16 Apr 2020 13:51:41 +0200},
biburl = {https://dblp.org/rec/journals/pacmpl/0001OV18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{coqnbe,
author = {Pawel Wieczorek and
Dariusz Biernacki},
editor = {June Andronick and
Amy P. Felty},
title = {A Coq formalization of normalization by evaluation for Martin-L{\"{o}}f
type theory},
booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2018, Los Angeles, CA, USA, January
8-9, 2018},
pages = {266--279},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3167091},
doi = {10.1145/3167091},
timestamp = {Sat, 19 Oct 2019 20:16:55 +0200},
biburl = {https://dblp.org/rec/conf/cpp/WieczorekB18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@Book{hottbook,
author = {The {Univalent Foundations Program}},
title = {Homotopy Type Theory: Univalent Foundations of Mathematics},
publisher = {\url{https://homotopytypetheory.org/book}},
address = {Institute for Advanced Study},
year = 2013}
@inproceedings{next700,
author = {Simon Boulier and
Pierre{-}Marie P{\'{e}}drot and
Nicolas Tabareau},
editor = {Yves Bertot and
Viktor Vafeiadis},
title = {The next 700 syntactical models of type theory},
booktitle = {Proceedings of the 6th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, {CPP} 2017, Paris, France, January 16-17, 2017},
pages = {182--194},
publisher = {{ACM}},
year = {2017},
url = {https://doi.org/10.1145/3018610.3018620},
doi = {10.1145/3018610.3018620},
timestamp = {Tue, 06 Nov 2018 16:59:23 +0100},
biburl = {https://dblp.org/rec/conf/cpp/BoulierPT17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{millerpattern,
author = {Dale Miller},
title = {A Logic Programming Language with Lambda-Abstraction, Function Variables,
and Simple Unification},
journal = {J. Log. Comput.},
volume = {1},
number = {4},
pages = {497--536},
year = {1991},
url = {https://doi.org/10.1093/logcom/1.4.497},
doi = {10.1093/logcom/1.4.497},
timestamp = {Mon, 29 Jul 2019 15:58:51 +0200},
biburl = {https://dblp.org/rec/journals/logcom/Miller91.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@book{harper2016practical,
title={Practical foundations for programming languages},
author={Harper, Robert},
year={2016},
publisher={Cambridge University Press}
}
@inproceedings{dybjer99finite,
author = {Peter Dybjer and
Anton Setzer},
editor = {Jean{-}Yves Girard},
title = {A Finite Axiomatization of Inductive-Recursive Definitions},
booktitle = {Typed Lambda Calculi and Applications, 4th International Conference,
TLCA'99, L'Aquila, Italy, April 7-9, 1999, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {1581},
pages = {129--146},
publisher = {Springer},
year = {1999},
url = {https://doi.org/10.1007/3-540-48959-2\_11},
doi = {10.1007/3-540-48959-2\_11},
timestamp = {Tue, 14 May 2019 10:00:41 +0200},
biburl = {https://dblp.org/rec/conf/tlca/DybjerS99.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{ziliani15unification,
author = {Beta Ziliani and
Matthieu Sozeau},
editor = {Kathleen Fisher and
John H. Reppy},
title = {A unification algorithm for Coq featuring universe polymorphism and
overloading},
booktitle = {Proceedings of the 20th {ACM} {SIGPLAN} International Conference on
Functional Programming, {ICFP} 2015, Vancouver, BC, Canada, September
1-3, 2015},
pages = {179--191},
publisher = {{ACM}},
year = {2015},
url = {https://doi.org/10.1145/2784731.2784751},
doi = {10.1145/2784731.2784751},
timestamp = {Tue, 06 Nov 2018 16:59:24 +0100},
biburl = {https://dblp.org/rec/conf/icfp/ZilianiS15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{timany18cumulative,
author = {Amin Timany and
Matthieu Sozeau},
editor = {H{\'{e}}l{\`{e}}ne Kirchner},
title = {Cumulative Inductive Types In Coq},
booktitle = {3rd International Conference on Formal Structures for Computation
and Deduction, {FSCD} 2018, July 9-12, 2018, Oxford, {UK}},
series = {LIPIcs},
volume = {108},
pages = {29:1--29:16},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2018},
url = {https://doi.org/10.4230/LIPIcs.FSCD.2018.29},
doi = {10.4230/LIPIcs.FSCD.2018.29},
timestamp = {Tue, 11 Feb 2020 15:52:14 +0100},
biburl = {https://dblp.org/rec/conf/rta/TimanyS18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{gratzer20multimodal,
author = {Daniel Gratzer and
G. A. Kavvos and
Andreas Nuyts and
Lars Birkedal},
editor = {Holger Hermanns and
Lijun Zhang and
Naoki Kobayashi and
Dale Miller},
title = {Multimodal Dependent Type Theory},
booktitle = {{LICS} '20: 35th Annual {ACM/IEEE} Symposium on Logic in Computer
Science, Saarbr{\"{u}}cken, Germany, July 8-11, 2020},
pages = {492--506},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3373718.3394736},
doi = {10.1145/3373718.3394736},
timestamp = {Sat, 05 Sep 2020 17:56:15 +0200},
biburl = {https://dblp.org/rec/conf/lics/GratzerKNB20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{kiselyov14metaocaml,
author = {Oleg Kiselyov},
editor = {Michael Codish and
Eijiro Sumii},
title = {The Design and Implementation of {BER} MetaOCaml - System Description},
booktitle = {Functional and Logic Programming - 12th International Symposium, {FLOPS}
2014, Kanazawa, Japan, June 4-6, 2014. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8475},
pages = {86--102},
publisher = {Springer},
year = {2014},
url = {https://doi.org/10.1007/978-3-319-07151-0\_6},
doi = {10.1007/978-3-319-07151-0\_6},
timestamp = {Tue, 14 May 2019 10:00:53 +0200},
biburl = {https://dblp.org/rec/conf/flops/Kiselyov14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{luo2012notes,
title={Notes on universes in type theory},
author={Luo, Zhaohui},
journal={Lecture notes for a talk at Institute for Advanced Study, Princeton (URL: http://www. cs. rhul. ac. uk/home/zhaohui/universes. pdf)},
pages={16},
year={2012}
}
@article{awodey18natural,
author = {Steve Awodey},
title = {Natural models of homotopy type theory},
journal = {Math. Struct. Comput. Sci.},
volume = {28},
number = {2},
pages = {241--286},
year = {2018},
url = {https://doi.org/10.1017/S0960129516000268},
doi = {10.1017/S0960129516000268},
timestamp = {Wed, 01 Apr 2020 08:48:37 +0200},
biburl = {https://dblp.org/rec/journals/mscs/Awodey18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{setzer00mahlo,
author = {Anton Setzer},
title = {Extending Martin-L{\"{o}}f Type Theory by one Mahlo-universe},
journal = {Arch. Math. Log.},
volume = {39},
number = {3},
pages = {155--181},
year = {2000},
url = {https://doi.org/10.1007/s001530050140},
doi = {10.1007/s001530050140},
timestamp = {Mon, 05 Jun 2017 20:48:09 +0200},
biburl = {https://dblp.org/rec/journals/aml/Setzer00.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{indexedir,
author = {Peter Dybjer and
Anton Setzer},
title = {Indexed induction-recursion},
journal = {J. Log. Algebraic Methods Program.},
volume = {66},
number = {1},
pages = {1--49},
year = {2006},
url = {https://doi.org/10.1016/j.jlap.2005.07.001},
doi = {10.1016/j.jlap.2005.07.001},
timestamp = {Tue, 16 Feb 2021 15:58:14 +0100},
biburl = {https://dblp.org/rec/journals/jlp/DybjerS06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{principia,
volume = {19},
journal = {Revue de M\'etaphysique et de Morale},
author = {A. N. Whitehead and B. Russell},
publisher = {Presses Universitaires de France},
pages = {19--19},
number = {2},
title = {Principia Mathematica},
year = {1911}
}
@article{harperpollack,
author = {Robert Harper and
Robert Pollack},
title = {Type Checking with Universes},
journal = {Theor. Comput. Sci.},
volume = {89},
number = {1},
pages = {107--136},
year = {1991},
url = {https://doi.org/10.1016/0304-3975(90)90108-T},
doi = {10.1016/0304-3975(90)90108-T},
timestamp = {Wed, 17 Feb 2021 22:01:21 +0100},
biburl = {https://dblp.org/rec/journals/tcs/HarperP91.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{universepolycoq,
author = {Matthieu Sozeau and
Nicolas Tabareau},
editor = {Gerwin Klein and
Ruben Gamboa},
title = {Universe Polymorphism in Coq},
booktitle = {Interactive Theorem Proving - 5th International Conference, {ITP}
2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,
Austria, July 14-17, 2014. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8558},
pages = {499--514},
publisher = {Springer},
year = {2014},
url = {https://doi.org/10.1007/978-3-319-08970-6\_32},
doi = {10.1007/978-3-319-08970-6\_32},
timestamp = {Tue, 14 May 2019 10:00:37 +0200},
biburl = {https://dblp.org/rec/conf/itp/SozeauT14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{positiveir,
author = {Neil Ghani and
Lorenzo Malatesta and
Fredrik Nordvall Forsberg},
title = {Positive Inductive-Recursive Definitions},
journal = {Log. Methods Comput. Sci.},
volume = {11},
number = {1},
year = {2015},
url = {https://doi.org/10.2168/LMCS-11(1:13)2015},
doi = {10.2168/LMCS-11(1:13)2015},
timestamp = {Thu, 25 Jun 2020 21:28:57 +0200},
biburl = {https://dblp.org/rec/journals/corr/GhaniMF15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{sprop,
author = {Ga{\"{e}}tan Gilbert and
Jesper Cockx and
Matthieu Sozeau and
Nicolas Tabareau},
title = {Definitional proof-irrelevance without {K}},
journal = {Proc. {ACM} Program. Lang.},
volume = {3},
number = {{POPL}},
pages = {3:1--3:28},
year = {2019},
url = {https://doi.org/10.1145/3290316},
doi = {10.1145/3290316},
timestamp = {Wed, 17 Feb 2021 08:54:00 +0100},
biburl = {https://dblp.org/rec/journals/pacmpl/GilbertCST19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{uemura,
author = {Taichi Uemura},
title = {A General Framework for the Semantics of Type Theory},
journal = {CoRR},
volume = {abs/1904.04097},
year = {2019},
url = {http://arxiv.org/abs/1904.04097},
eprinttype = {arXiv},
eprint = {1904.04097},
timestamp = {Thu, 14 Oct 2021 09:15:56 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1904-04097.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{bocquet2021relative,
title={Relative induction principles for type theories},
author={Bocquet, Rafa{\"e}l and Kaposi, Ambrus and Sattler, Christian},
journal={arXiv preprint arXiv:2102.11649},
year={2021}
}
@inproceedings{cubicalnorm,
author = {Jonathan Sterling and
Carlo Angiuli},
title = {Normalization for Cubical Type Theory},
booktitle = {36th Annual {ACM/IEEE} Symposium on Logic in Computer Science, {LICS}
2021, Rome, Italy, June 29 - July 2, 2021},
pages = {1--15},
publisher = {{IEEE}},
year = {2021},
url = {https://doi.org/10.1109/LICS52264.2021.9470719},
doi = {10.1109/LICS52264.2021.9470719},
timestamp = {Thu, 14 Oct 2021 09:50:17 +0200},
biburl = {https://dblp.org/rec/conf/lics/SterlingA21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@incollection{aczel1977introduction,
title={An introduction to inductive definitions},
author={Aczel, Peter},
booktitle={Studies in Logic and the Foundations of Mathematics},
volume={90},
pages={739--782},
year={1977},
publisher={Elsevier}
}
@phdthesis{thorstenthesis,
author = {Thorsten Altenkirch},
title = {Constructions, inductive types and strong normalization},
school = {University of Edinburgh, {UK}},
year = {1993},
timestamp = {Tue, 09 Jul 2019 17:08:12 +0200},
biburl = {https://dblp.org/rec/books/daglib/0072947.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/bit/Nordstrom88,
author = {Bengt Nordstr{\"{o}}m},
title = {Terminating General Recursion},
journal = {{BIT}},
volume = {28},
number = {3},
pages = {605--619},
year = {1988},
url = {https://doi.org/10.1007/BF01941137},
doi = {10.1007/BF01941137},
timestamp = {Tue, 22 Jun 2021 13:02:26 +0200},
biburl = {https://dblp.org/rec/journals/bit/Nordstrom88.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{mcbride2015datatypes,
title={Datatypes of datatypes},
author={McBride, Conor},
journal={Summer School on Generic and Effectful Programming, St Anne’s College, Oxford},
year={2015}
}