Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2017.4
URN: urn:nbn:de:0030-drops-100521
URL: https://drops.dagstuhl.de/opus/volltexte/2018/10052/
Lepigre, Rodolphe
PML2: Integrated Program Verification in ML
| pdf-format: |
|
Abstract
We present the PML_2 language, which provides a uniform environment for programming, and for proving properties of programs in an ML-like setting. The language is Curry-style and call-by-value, it provides a control operator (interpreted in terms of classical logic), it supports general recursion and a very general form of (implicit, non-coercive) subtyping. In the system, equational properties of programs are expressed using two new type formers, and they are proved by constructing terminating programs. Although proofs rely heavily on equational reasoning, equalities are exclusively managed by the type-checker. This means that the user only has to choose which equality to use, and not where to use it, as is usually done in mathematical proofs. In the system, writing proofs mostly amounts to applying lemmas (possibly recursive function calls), and to perform case analyses (pattern matchings).
BibTeX - Entry
@InProceedings{lepigre:LIPIcs:2018:10052,
author = {Rodolphe Lepigre},
title = {{PML2: Integrated Program Verification in ML}},
booktitle = {23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
pages = {4:1--4:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-071-2},
ISSN = {1868-8969},
year = {2018},
volume = {104},
editor = {Andreas Abel and Fredrik Nordvall Forsberg and Ambrus Kaposi},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2018/10052},
URN = {urn:nbn:de:0030-drops-100521},
doi = {10.4230/LIPIcs.TYPES.2017.4},
annote = {Keywords: program verification, classical logic, ML-like language, termination checking, Curry-style quantification, implicit subtyping}
}
| Keywords: | program verification, classical logic, ML-like language, termination checking, Curry-style quantification, implicit subtyping | |
| Seminar: | 23rd International Conference on Types for Proofs and Programs (TYPES 2017) | |
| Issue date: | 2018 | |
| Date of publication: | 08.01.2019 |
