add bib
This commit is contained in:
parent
d4ad899b2e
commit
aff0748d82
1 changed files with 145 additions and 0 deletions
145
quox.bib
Normal file
145
quox.bib
Normal file
|
|
@ -0,0 +1,145 @@
|
|||
% 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, 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},
|
||||
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},
|
||||
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}
|
||||
}
|
||||
|
||||
|
||||
% Misc implementation
|
||||
|
||||
@article{nbe-abel,
|
||||
title = {Normalization by Evaluation for Martin-Löf 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},
|
||||
}
|
||||
|
||||
@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}
|
||||
}
|
||||
Loading…
Reference in a new issue