@inproceedings{accattoli12cpp,
author = {Beniamino Accattoli},
title = {Proof pearl: Abella formalization of lambda calculus
cube property},
booktitle = {Second International Conference on Certified Programs
and Proofs},
editor = {Chris Hawblitzel and Dale Miller},
year = {2012},
publisher = {Springer},
series = {LNCS},
volume = {7679},
pages = {173--187}
}
@inproceedings{accattoli23itp,
author = {Beniamino Accattoli and Horace Blanc and Claudio
Sacerdoti Coen},
title = {{Formalizing Functions as Processes}},
booktitle = {14th International Conference on Interactive Theorem
Proving (ITP 2023)},
pages = {5:1--5:21},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
year = {2023},
volume = {268},
editor = {Adam Naumowicz and Ren\'{e} Thiemann},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r
Informatik},
address = {Dagstuhl, Germany},
url = {https://drops.dagstuhl.de/opus/volltexte/2023/18380},
urn = {urn:nbn:de:0030-drops-183800},
doi = {10.4230/LIPIcs.ITP.2023.5}
}
@article{balabonski23lmcs,
title = {{A strong call-by-need calculus}},
author = {Thibaut Balabonski and Antoine Lanco and Guillaume
Melquiond},
url = {https://lmcs.episciences.org/11115},
doi = {10.46298/lmcs-19(1:21)2023},
journal = {{Logical Methods in Computer Science}},
volume = {{Volume 19, Issue 1}},
year = {2023},
month = mar
}
@inproceedings{chaudhuri15cpp,
author = {Kaustuv Chaudhuri and Matteo Cimini and Dale Miller},
title = {A Lightweight Formalization of the Metatheory of
Bisimulation-Up-To},
booktitle = {Proceedings of the 4th ACM-SIGPLAN Conference on
Certified Programs and Proofs},
doi = {10.1145/2676724.2693170},
year = {2015},
editor = {Xavier Leroy and Alwen Tiu},
pages = {157--166},
month = jan,
address = {Mumbai, India},
publisher = {ACM},
url = {https://hal.inria.fr/hal-01091524/document}
}
@inproceedings{chaudhuri16lsfa,
author = {Kaustuv Chaudhuri and Leonardo Lima and Giselle Reis},
title = {Formalized Meta-Theory of Sequent Calculi for
Substructural Logics},
booktitle = {Workshop on Logical and Semantic Frameworks, with
Applications (LSFA)},
year = {2016},
note = {Post proceedings version to appear; Formalization
\url{https://github.com/meta-logic/abella-reasoning}}
}
@inproceedings{cimini20sle,
author = {Matteo Cimini and Dale Miller and Jeremy G. Siek},
title = {Extrinsically Typed Operational Semantics for
Functional Languages},
booktitle = {ACM SIGPLAN International Conference on Software
Language Engineering (SLE)},
year = {2020},
pages = {108--125},
editor = {Laurence Tratt and Juan de Lara},
doi = {10.1145/3426425.3426936},
month = nov,
organization = {ACM SIGPLAN},
publisher = {ACM}
}
@article{felty15jar,
author = {Amy P. Felty and Alberto Momigliano and Brigitte
Pientka},
title = {The Next 700 Challenge Problems for Reasoning with
Higher-Order Abstract Syntax Representations: Part
2--{A} Survey},
journal = {J. of Automated Reasoning},
year = {2015},
volume = {55},
number = {4},
pages = {307--372},
doi = {10.1007/s10817-015-9327-3}
}
@article{forster19jfp,
author = {Yannick Forster and Ohad Kammar and Sam Lindley and
Matija Pretnar},
title = {On the expressive power of user-defined effects:
effect handlers, monadic reflection, delimited
control},
journal = {Journal of Functional Programming},
year = {2019},
volume = {29},
url = {http://homepages.inf.ed.ac.uk/slindley/papers/effmondel-jfp.pdf}
}
@inproceedings{kaiser17fscd,
title = {Relating System {F} and $\lambda$2: {A} Case Study in
{Coq}, {Abella} and {Beluga}},
author = {Jonas Kaiser and Brigitte Pientka and Gert Smolka},
booktitle = {{FSCD 2017 - 2nd International Conference on Formal
Structures for Computation and Deduction}},
address = {Oxford, UK},
year = {2017},
editor = {Dale Miller},
month = sep,
doi = {10.4230/LIPIcs.FSCD.2017.21},
pages = {21:1--21:19}
}
@inproceedings{momigliano12lfmtp,
author = {Alberto Momigliano},
title = {A supposedly fun thing {I} may have to do again: a
{HOAS} encoding of {Howe's} method},
booktitle = {Proceedings of LFMTP'12},
year = {2012},
pages = {33--42},
publisher = {ACM},
doi = {10.1145/3426425.3426936}
}
@inproceedings{wang16esop,
author = {Yuting Wang and Gopalan Nadathur},
title = {A Higher-Order Abstract Syntax Approach to Verified
Transformations on Functional Programs},
booktitle = {Programming Languages and Systems. ESOP 2016},
year = {2016},
editor = {P. Thiemann},
number = {9632},
series = {LNCS},
publisher = {Springer},
pages = {752--779},
url = {https://arxiv.org/abs/1509.03705}
}
@phdthesis{wang16phd,
author = {Yuting Wang},
title = {A Higher-Order Abstract Syntax Approach to the
Verified Compilation of Functional Programs},
school = {University of Minnesota},
year = {2016},
month = dec,
url = {https://arxiv.org/abs/1702.03363}
}
@inproceedings{zhao18itp,
author = {Jinxu Zhao and Bruno C. d. S. Oliveira and Tom
Schrijvers},
title = {Formalization of a Polymorphic Subtyping Algorithm},
booktitle = {International Conference on Interactive Theorem
Proving (ITP 2018)},
year = {2018},
number = {10895},
series = {LNCS},
pages = {604--622},
doi = {10.1007/978-3-319-94821-8_36}
}
@inproceedings{zhao19icfp,
author = {Jinxu Zhao and Bruno C. d. S. Oliveira and Tom
Schrijvers},
title = {A mechanical formalization of higher-ranked
polymorphic type inference},
booktitle = {Proceedings of the {ACM} on Programming Languages},
year = {2019},
volume = {3},
number = {112},
series = {ICFP},
pages = {1--29},
month = jul,
doi = {10.1145/3341716}
}
@phdthesis{zhao21phd,
author = {Jinxu Zhao},
title = {Formalized Higher-Ranked Polymorphic Type Inference
Algorithms},
school = {University of Hong Kong},
year = {2021},
month = jul,
url = {https://i.cs.hku.hk/~bruno/thesis/JinxuZhao.pdf}
}
This file was generated by bibtex2html 1.99.