quox/quox.bib

202 lines
7.3 KiB
BibTeX

% quantitative stuff
@inproceedings{grtt,
author = {Moon, Benjamin and
Eades, III, Harley and
Orchard, Dominic},
editor = {Yoshida, Nobuko},
title = {Graded Modal Dependent Type Theory},
booktitle = {Programming Languages and Systems:
30th European Symposium on Programming, ({ESOP} 2021)},
series = {Lecture Notes in Computer Science},
volume = {12648},
pages = {462--490},
publisher = {Springer},
year = {2021},
% url = {https://doi.org/10.1007/978-3-030-72019-3\_17},
url = {https://arxiv.org/abs/2010.13163},
doi = {10.1007/978-3-030-72019-3\_17}
}
@inproceedings{nuttin,
author = {Conor McBride},
editor = {Sam Lindley and
Conor McBride and
Philip W. Trinder and
Donald Sannella},
title = {I Got Plenty o' Nuttin'},
booktitle = {A List of Successes That Can Change the World - Essays Dedicated to
Philip Wadler on the Occasion of His 60th Birthday},
series = {Lecture Notes in Computer Science},
volume = {9600},
pages = {207--233},
publisher = {Springer},
year = {2016},
% url = {https://doi.org/10.1007/978-3-319-30936-1\_12},
url = {https://personal.cis.strath.ac.uk/conor.mcbride/PlentyO-CR.pdf},
doi = {10.1007/978-3-319-30936-1\_12}
}
@inproceedings{qtt,
author = {Robert Atkey},
editor = {Anuj Dawar and
Erich Gr{\"{a}}del},
title = {Syntax and Semantics of Quantitative Type Theory},
booktitle = {Proceedings of the 33rd Annual {ACM/IEEE} Symposium on Logic in Computer
Science, {LICS} 2018, Oxford, UK, July 09-12, 2018},
pages = {56--65},
publisher = {{ACM}},
year = {2018},
% url = {https://doi.org/10.1145/3209108.3209189},
url = {https://bentnib.org/quantitative-type-theory.pdf},
doi = {10.1145/3209108.3209189}
}
% observational stuff
@inproceedings{ott-now,
author = {Thorsten Altenkirch and
Conor McBride and
Wouter Swierstra},
editor = {Aaron Stump and
Hongwei Xi},
title = {Observational equality, now!},
booktitle = {Proceedings of the {ACM} Workshop Programming Languages meets Program
Verification, {PLPV} 2007, Freiburg, Germany, October 5, 2007},
pages = {57--68},
publisher = {{ACM}},
year = {2007},
% url = {https://doi.org/10.1145/1292597.1292608},
url = {https://www.cs.nott.ac.uk/~psztxa/publ/obseqnow.pdf},
doi = {10.1145/1292597.1292608}
}
@inproceedings{xtt,
author = {Jonathan Sterling and
Carlo Angiuli and
Daniel Gratzer},
editor = {Herman Geuvers},
title = {Cubical Syntax for Reflection-Free Extensional Equality},
booktitle = {4th International Conference on Formal Structures for Computation
and Deduction, {FSCD} 2019, June 24-30, 2019, Dortmund, Germany},
series = {LIPIcs},
volume = {131},
pages = {31:1--31:25},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2019},
% url = {https://doi.org/10.4230/LIPIcs.FSCD.2019.31},
url = {https://arxiv.org/pdf/1904.08562.pdf},
doi = {10.4230/LIPIcs.FSCD.2019.31}
}
% NbE
@article{nbe-mltt,
title = {Normalization by Evaluation for Martin-L\"of Type Theory with
One Universe},
journal = {Electronic Notes in Theoretical Computer Science},
volume = {173},
pages = {17-39},
year = {2007},
note = {Proceedings of the 23rd Conference on the Mathematical Foundations
of Programming Semantics (MFPS XXIII)},
issn = {1571-0661},
doi = {https://doi.org/10.1016/j.entcs.2007.02.025},
url = {https://www.sciencedirect.com/science/article/pii/S1571066107000977},
author = {Andreas Abel and Klaus Aehlig and Peter Dybjer},
keywords = {Dependent Types, Domain Semantics, Normalization by Evaluation,
Type Theory, Universe}
}
@inproceedings{nbe-mltt-eq,
author = {Andreas Abel and Thierry Coquand and Peter Dybjer},
title = {Normalization by Evaluation for Martin-L\"of Type Theory with Typed
Equality Judgements},
booktitle = {22nd {IEEE} Symposium on Logic in Computer Science
({LICS} 2007)},
pages = {3--12},
publisher = {{IEEE} Computer Society},
year = {2007},
% url = {https://doi.org/10.1109/LICS.2007.33},
url = {https://www.cse.chalmers.se/~abela/lics07.pdf},
doi = {10.1109/LICS.2007.33}
}
@inproceedings{nbe-cbpv,
author = {Andreas Abel and Christian Sattler},
editor = {Ekaterina Komendantskaya},
title = {Normalization by Evaluation for Call-By-Push-Value and Polarized
Lambda Calculus},
booktitle = {Proceedings of the 21st International Symposium on Principles and
Practice of Programming Languages ({PPDP} 2019)},
pages = {3:1--3:12},
publisher = {{ACM}},
year = {2019},
% url = {https://doi.org/10.1145/3354166.3354168},
url = {https://www.cse.chalmers.se/~abela/ppdp19.pdf},
doi = {10.1145/3354166.3354168}
}
@phdthesis{nbe-habil,
author = {Andreas Abel},
title = {Normalization by Evaluation: Dependent Types and Impredicativity},
year = {2013},
type = {Habilitation thesis},
school = {Institut f\"ur Informatik,
Ludwig-Maximilians-Universit\"at M\"unchen},
url = {https://www.cse.chalmers.se/~abela/habil.pdf}
}
@inproceedings{nbe-delay,
author = {Andreas Abel and James Chapman},
editor = {Paul Levy and Neel Krishnaswami},
title = {Normalization by Evaluation in the Delay Monad:
{A} Case Study for Coinduction via Copatterns and Sized Types},
booktitle = {Proceedings 5th Workshop on Mathematically Structured
Functional Programming (MSFP 2014)},
series = {{EPTCS}},
volume = {153},
pages = {51--67},
year = {2014},
% url = {https://doi.org/10.4204/EPTCS.153.4},
url = {https://www.cse.chalmers.se/~abela/eptcs14.pdf},
doi = {10.4204/EPTCS.153.4}
}
% Misc implementation
@article{expl-sub,
author = {Mart{\'{\i}}n Abadi and
Luca Cardelli and
Pierre{-}Louis Curien and
Jean{-}Jacques L{\'{e}}vy},
title = {Explicit Substitutions},
journal = {J. Funct. Program.},
volume = {1},
number = {4},
pages = {375--416},
year = {1991},
% url = {https://doi.org/10.1017/S0956796800000186},
url = {http://lucacardelli.name/Papers/ExplicitSub.pdf},
doi = {10.1017/S0956796800000186}
}
@article{modal-mltt,
author = {Gratzer, Daniel and Sterling, Jonathan and Birkedal, Lars},
location = {New York, NY, USA},
publisher = {ACM},
date = {2019-07},
doi = {10.1145/3341711},
issn = {2475-1421},
journaltitle = {Proceedings of the ACM on Programming Languages},
keywords = {Modal types,dependent types,normalization by evaluation,type-checking},
number = {ICFP},
pages = {107:1--107:29},
title = {Implementing a Modal Dependent Type Theory},
volume = {3},
url = {https://www.jonmsterling.com/pdfs/modal-mltt.pdf},
note = {implementation at
\url{https://www.jonmsterling.com/resources/blott.tar.gz}}
}