Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)
Thibaut Balabonski, Antoine Lanco, and Guillaume Melquiond. A Strong Call-By-Need Calculus. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 9:1-9:22, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@InProceedings{balabonski_et_al:LIPIcs.FSCD.2021.9, author = {Balabonski, Thibaut and Lanco, Antoine and Melquiond, Guillaume}, title = {{A Strong Call-By-Need Calculus}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {9:1--9:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.9}, URN = {urn:nbn:de:0030-drops-142477}, doi = {10.4230/LIPIcs.FSCD.2021.9}, annote = {Keywords: strong reduction, call-by-need, evaluation strategy, normalization} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Guillaume Bertholon, Érik Martin-Dorel, and Pierre Roux. Primitive Floats in Coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 7:1-7:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
@InProceedings{bertholon_et_al:LIPIcs.ITP.2019.7, author = {Bertholon, Guillaume and Martin-Dorel, \'{E}rik and Roux, Pierre}, title = {{Primitive Floats in Coq}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {7:1--7:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-122-1}, ISSN = {1868-8969}, year = {2019}, volume = {141}, editor = {Harrison, John and O'Leary, John and Tolmach, Andrew}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.7}, URN = {urn:nbn:de:0030-drops-110629}, doi = {10.4230/LIPIcs.ITP.2019.7}, annote = {Keywords: Coq formal proofs, floating-point arithmetic, reflexive tactics, Cholesky decomposition} }
Published in: Dagstuhl Seminar Proceedings, Volume 6021, Reliable Implementation of Real Number Algorithms: Theory and Practice (2006)
Sylvain Pion, Hervé Brönnimann, and Guillaume Melquiond. A Proposal to add Interval Arithmetic to the C++ Standard Library. In Reliable Implementation of Real Number Algorithms: Theory and Practice. Dagstuhl Seminar Proceedings, Volume 6021, pp. 1-25, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2006)
@InProceedings{pion_et_al:DagSemProc.06021.4, author = {Pion, Sylvain and Br\"{o}nnimann, Herv\'{e} and Melquiond, Guillaume}, title = {{A Proposal to add Interval Arithmetic to the C++ Standard Library}}, booktitle = {Reliable Implementation of Real Number Algorithms: Theory and Practice}, pages = {1--25}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2006}, volume = {6021}, editor = {Peter Hertling and Christoph M. Hoffmann and Wolfram Luther and Nathalie Revol}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06021.4}, URN = {urn:nbn:de:0030-drops-7189}, doi = {10.4230/DagSemProc.06021.4}, annote = {Keywords: Interval arithmetic, C++, ISO standard} }
Feedback for Dagstuhl Publishing