Document Open Access Logo

PML2: Integrated Program Verification in ML

Author Rodolphe Lepigre

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2017.4.pdf
  • Filesize: 0.51 MB
  • 27 pages

Document Identifiers

Author Details

Rodolphe Lepigre
  • LAMA, CNRS, Université Savoie Mont Blanc, France & , Inria, LSV, CNRS, Université Paris-Saclay, France

Cite AsGet BibTex

Rodolphe Lepigre. PML2: Integrated Program Verification in ML. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 4:1-4:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.TYPES.2017.4

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).

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software verification
Keywords
  • program verification
  • classical logic
  • ML-like language
  • termination checking
  • Curry-style quantification
  • implicit subtyping

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Andreas Abel. Semi-Continuous Sized Types and Termination. Logical Methods in Computer Science, 4(2), 2008. Google Scholar
  2. Sylvain Baro. Conception et implémentation d'un système d'aide à la spécification et à la preuve de programmes ML. PhD thesis, Paris Diderot University, France, 2003. Google Scholar
  3. Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich. Combining proofs and programs in a dependently typed language. In POPL, pages 33-46. ACM, 2014. Google Scholar
  4. Arthur Charguéraud. Program verification through characteristic formulae. In ICFP, pages 321-332. ACM, 2010. Google Scholar
  5. Arthur Charguéraud. Characteristic formulae for the verification of imperative programs. In ICFP, pages 418-430. ACM, 2011. Google Scholar
  6. Robert L. Constable, Stuart F. Allen, Mark Bromley, Rance Cleaveland, J. F. Cremer, R. W. Harper, Douglas J. Howe, Todd B. Knoblock, N. P. Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith. Implementing mathematics with the Nuprl proof development system. Prentice Hall, 1986. Google Scholar
  7. Thierry Coquand and Gérard P. Huet. The Calculus of Constructions. Inf. Comput., 76(2/3):95-120, 1988. Google Scholar
  8. Jacques Garrigue. Programming with polymorphic variants. In ML Workshop, 1998. Google Scholar
  9. Jean-Yves Girard. Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur. PhD thesis, Université Paris 7, 1972. Google Scholar
  10. Timothy Griffin. A Formulae-as-Types Notion of Control. In POPL, pages 47-58. ACM Press, 1990. Google Scholar
  11. Robert Harper and Mark Lillibridge. ML with callcc is unsound. Posted to the SML mailing list, 1991. URL: http://www.seas.upenn.edu/~sweirich/types/archive/1991/msg00034.html.
  12. Douglas J. Howe. Equality In Lazy Computation Systems. In LICS, pages 198-203. IEEE Computer Society, 1989. Google Scholar
  13. John Hughes, Lars Pareto, and Amr Sabry. Proving the Correctness of Reactive Systems Using Sized Types. In POPL, pages 410-423. ACM Press, 1996. Google Scholar
  14. Limin Jia, Jeffrey A. Vaughan, Karl Mazurak, Jianzhou Zhao, Luke Zarko, Joseph Schorr, and Steve Zdancewic. AURA: a programming language for authorization and audit. In ICFP, pages 27-38. ACM, 2008. Google Scholar
  15. Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. The size-change principle for program termination. In POPL, pages 81-92. ACM, 2001. Google Scholar
  16. Rodolphe Lepigre. A Classical Realizability Model for a Semantical Value Restriction. In ESOP, volume 9632 of Lecture Notes in Computer Science, pages 476-502. Springer, 2016. Google Scholar
  17. Rodolphe Lepigre. Semantics and Implementation of an Extension of ML for Proving Programs. (Sémantique et Implantation d'une Extension de ML pour la Preuve de Programmes). PhD thesis, Grenoble Alpes University, France, 2017. Google Scholar
  18. Rodolphe Lepigre and Christophe Raffalli. Implementation of the PML₂ language. The source code is available on GitHub at https://github.com/rlepigre/pml, 2017.
  19. Rodolphe Lepigre and Christophe Raffalli. Practical Subtyping for Curry-Style Languages. to appear in ACM Trans. Program. Lang. Syst., 2018. Draft and joined implementation available at URL: https://rlepigre.github.io/subml/.
  20. Daniel R. Licata and Robert Harper. Positively dependent types. In PLPV, pages 3-14. ACM, 2009. Google Scholar
  21. Pascal Manoury, Michel Parigot, and Marianne Simonot. ProPre A Programming Language with Proofs. In LPAR, volume 624 of Lecture Notes in Computer Science, pages 484-486. Springer, 1992. Google Scholar
  22. Per Martin-Löf. Constructive mathematics and computer programming. In L. Jonathan Cohen, Jerzy Łoś, Helmut Pfeiffer, and Klaus-Peter Podewski, editors, Logic, Methodology and Philosophy of Science VI, volume 104 of Studies in Logic and the Foundations of Mathematics, pages 153-175. North-Holland, 198. Google Scholar
  23. The Coq development team. The Coq proof assistant reference manual. LogiCal Project, 2018. Version 8.8.0. URL: http://coq.inria.fr.
  24. Ulf Norell. Dependently Typed Programming in Agda. In Advanced Functional Programming, volume 5832 of Lecture Notes in Computer Science, pages 230-266. Springer, 2008. Google Scholar
  25. Michel Parigot. Lambda-Mu-Calculus: An Algorithmic Interpretation of Classical Natural Deduction. In LPAR, volume 624 of Lecture Notes in Computer Science, pages 190-201. Springer, 1992. Google Scholar
  26. Christophe Raffalli. Getting results from programs extracted from classical proofs. Theor. Comput. Sci., 323(1-3):49-70, 2004. Google Scholar
  27. Christophe Raffalli. PML: a new proof assistant. Prototype implementation available at http://lama.univ-savoie.fr/~raffalli/pml, talk at the TYPES workshop, 2007.
  28. John C. Reynolds. Towards a Theory of Type Structure. In Programming Symposium, Proceedings Colloque sur la Programmation, pages 408-423. Springer-Verlag, 1974. Google Scholar
  29. Yann Régis-Gianas. From types to logical assertions : automatic or assisted proofs of property about functional programs. (Des types aux assertions logiques : preuve automatique ou assistée de propriétés sur les programmes fonctionnels). PhD thesis, Paris Diderot University, France, 2007. Google Scholar
  30. Jorge Luis Sacchini. Type-Based Productivity of Stream Definitions in the Calculus of Constructions. In LICS, pages 233-242. IEEE Computer Society, 2013. Google Scholar
  31. Ronan Saillard. Typechecking in the lambda-Pi-Calculus Modulo : Theory and Practice. (Vérification de typage pour le lambda-Pi-Calcul Modulo : théorie et pratique). PhD thesis, Mines ParisTech, France, 2015. Google Scholar
  32. Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, and Jean Yang. Secure distributed programming with value-dependent types. J. Funct. Program., 23(4):402-451, 2013. Google Scholar
  33. Philip Wadler. Call-by-value is dual to call-by-name. SIGPLAN Notices, 38(9):189-201, 2003. Google Scholar
  34. Andrew K. Wright. Simple Imperative Polymorphism. Lisp and Symbolic Computation, 8(4):343-355, 1995. Google Scholar
  35. Andrew K. Wright and Matthias Felleisen. A Syntactic Approach to Type Soundness. Inf. Comput., 115(1):38-94, 1994. Google Scholar
  36. Hongwei Xi. Applied Type System: Extended Abstract. In TYPES, volume 3085 of Lecture Notes in Computer Science, pages 394-408. Springer, 2003. Google Scholar
  37. Hongwei Xi and Frank Pfenning. Dependent Types in Practical Programming. In POPL, pages 214-227. ACM, 1999. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact