|
|
Publications
A Formalization of SQL with Nulls
with James Cheney
Submitted.
[arXiv]
[GitHub]
Query Lifting: Language-integrated query for heterogeneous nested collections
with James Cheney
Programming Languages and Systems. ESOP 2021. LNCS, Volume 12648, pages 579-606, Springer, 2021. DOI: 10.1007/978-3-030-72019-3_21
[arXiv]
Strongly Normalizing Higher-Order Relational Queries
with James Cheney
5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), LIPIcs, Volume 167, pages 28:1-28:22,
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2020, DOI: 10.4230/LIPIcs.FSCD.2020.28.
[preprint]
Mixing set and bag semantics
with James Cheney
Proceedings of the 17th ACM SIGPLAN International Symposium on Database Programming Languages (DBPL 2019), pages 70-73, ACM, 2019, DOI: 10.1145/3315507.3330202.
[arXiv]
Explicit Auditing
with James Cheney
Proceedings of the 15th International Colloquium on Theoretical Aspects of Computing (ICTAC 2018), pages 376-395, Springer, 2018, DOI: 10.1007/978-3-030-02508-3_20.
[arXiv]
A Core Calculus for Provenance Inspection
Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming (PPDP 2017), pages 187-198, ACM, 2017, DOI: 10.1145/3131851.3131871.
[download PDF (extended version)]
Strongly Normalizing Audited Computation
with James Cheney
26th EACSL Annual Conference on Computer Science Logic (CSL 2017). LIPIcs, Volume 82, pages 36:1-36:21, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017, DOI:10.4230/LIPIcs.CSL.2017.36.
[arXiv]
Imperative Functional Programs That Explain Their Work
with Jan Stolarek, Roly Perera, James Cheney
International Conference on Functional Programming (ICFP 2017). Proceedings of the ACM on Programming Languages, Volume 1(ICFP), pages 14:1-14:28, ACM, 2017, DOI:10.1145/3110258.
[arXiv]
Abstracting an Operational Semantics to Finite Automata
with Nadezhda Baklanova, Jan-Georg Smaus, Martin Strecker
ICTERI 2015, revised selected papers, CCIS, Volume 594, pages 109-123, Springer, 2016.
[arXiv]
A Formalization of Multi-tape Turing Machines
with Andrea Asperti
Published in Theoretical Computer Science, volume 603(C), pages 23-42, October 2015, DOI:10.1016/j.tcs.2015.07.013.
[download PDF]
Matita Tutorial
with Andrea Asperti, Claudio Sacerdoti Coen
Published in the Journal of Formalized Reasoning, volume 7(2), pages 91-199, 2014, DOI:10.6092/issn.1972-5787/4651.
[download PDF]
Binding Structures as an Abstract Data Type
European Symposium on Programming Languages and Systems (ESOP 2015). LNCS, Volume 9032, pages 762-786, Springer, 2015, DOI: 10.1007/978-3-662-46669-8_31.
[download PDF]
A Proof of Bertrand's Postulate
with Andrea Asperti
Published in the Journal of Formalized Reasoning, volume 5, pages 37-57, 2012, ISSN: 1972-5787.
[download PDF]
Rating Disambiguation Errors
with Andrea Asperti
Proceedings of the 2nd International Conference on Certified Programs and Proofs (CPP 2012), LNCS,
Volume 7679, Pages 240--255, Springer, 2012.
[download PDF]
Formalizing Turing Machines
with Andrea Asperti
Proceedings of the 19th Workshop on Logic, Language, Information and Computation (WoLLIC 2012), LNCS,
Volume 7456, Pages 1--25, Springer, 2012.
[download PDF]
A Web Interface for Matita
with Andrea Asperti
Proceedings of the Conference on Intelligent Computer Mathematics (CICM 2012),
LNAI, Volume 7362/2012, Pages 417-421, DOI:10.1007/978-3-642-31374-5_28, ISBN
978-3-642-31373-8.
[download PDF]
A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive
Constructions
with Andrea Asperti, Claudio Sacerdoti Coen, and Enrico Tassi
Published in Logical Methods in Computer Science, volume 8, Pages 1-49, 2012.
DOI:10.2168/LMCS-8(1:18)2012. ISSN: 1860-5974.
[download PDF]
The Matita Interactive Theorem Prover
with Andrea Asperti, Claudio Sacerdoti Coen, and Enrico Tassi
23rd International Conference on Automated Deduction, CADE 2011
[download PDF]
Formal Metatheory of Programming Languages in the Matita Interactive Theorem
Prover
with Andrea Asperti, Claudio Sacerdoti Coen, and Enrico Tassi
Published in the Journal of Automated Reasoning, special issue on the PoplMark
challenge, volume 49(3), pages 427-451, October 2012, DOI
10.1007/s10817-011-9228-z.
[download PDF]
A Canonical Locally Named Representation of Binding
with Randy Pollack, Masahiko Sato
Published in the Journal of Automated Reasoning, special issue on Theory and
Applications of Abstraction, Substitution and Naming, volume 49(2), pages
185-207, August 2012, DOI 10.1007/s10817-011-9229-y.
[download PDF]
A new type for tactics
with Andrea Asperti, Claudio Sacerdoti Coen, and Enrico Tassi
To appear in the proceedings of ACM SIGSAM PLMMS 2009, ISBN 978-1-60558-735-6. Published as technical report UBLCS-2009-14.
[download PDF]
Hints in Unification
with Andrea Asperti, Claudio Sacerdoti Coen, and Enrico Tassi
Published in the proceedings of TPHOLs 2009, LNCS, Volume 5674/2009, Pages 84-98, DOI 10.1007/978-3-642-03359-9, ISBN 978-3-642-03358-2
[download PDF]
A compact kernel for the calculus of inductive constructions
with Andrea Asperti, Claudio Sacerdoti Coen, and Enrico Tassi
Published in the Journal Sadhana, Volume 34, Pages 71-144, Year 2009. ISSN: 0256-2499
[download PDF]
About the formalization of some results by Chebyshev in number theory
with Andrea Asperti
Proceedings of TYPES'08, LNCS, Vol. 5497/2009, pages 19-31, DOI
10.1007/978-3-642-02444-3, ISBN 978-3-642-02443-6
[download PDF]
PhD thesis
Theoretical and Implementation Aspects in the Mechanization of the Metatheory of Programming Languages
[download PDF]
A VirtualBox image (tested on VirtualBox v.4.0.0 r69151) of the Matita
interactive theorem prover including the formalizations described in the
thesis can be downloaded
here.
|
