add more bib entries

This commit is contained in:
rhiannon morris 2021-09-25 20:10:30 +02:00
parent 83ad802f6e
commit f87950915d
1 changed files with 68 additions and 12 deletions

View File

@ -6,20 +6,18 @@
Orchard, Dominic},
editor = {Yoshida, Nobuko},
title = {Graded Modal Dependent Type Theory},
booktitle = {Programming Languages and Systems - 30th European Symposium on Programming,
{ESOP} 2021, Held as Part of the European Joint Conferences on Theory
and Practice of Software, {ETAPS} 2021, Luxembourg City, Luxembourg,
March 27 - April 1, 2021, Proceedings},
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://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
@ -93,10 +91,10 @@
}
% Misc implementation
% NbE
@article{nbe-abel,
title = {Normalization by Evaluation for Martin-Löf Type Theory with
@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},
@ -109,9 +107,66 @@
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},
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
@ -125,7 +180,7 @@
year = {1991},
% url = {https://doi.org/10.1017/S0956796800000186},
url = {http://lucacardelli.name/Papers/ExplicitSub.pdf},
doi = {10.1017/S0956796800000186},
doi = {10.1017/S0956796800000186}
}
@article{modal-mltt,
@ -142,5 +197,6 @@
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}}
note = {implementation at
\url{https://www.jonmsterling.com/resources/blott.tar.gz}}
}