Document Open Access Logo

A Few Lessons from the Mezzo Project

Authors Francois Pottier, Jonathan Protzenko

PDF
Thumbnail PDF

File

LIPIcs.SNAPL.2015.221.pdf
  • Filesize: 0.53 MB
  • 17 pages

Document Identifiers

Author Details

Francois Pottier
Jonathan Protzenko

Cite As Get BibTex

Francois Pottier and Jonathan Protzenko. A Few Lessons from the Mezzo Project. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 221-237, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.SNAPL.2015.221

Abstract

With Mezzo, we set out to design a new, better programming language. In this modest document, we recount our adventure: what worked, and what did not; the decisions that appear in hindsight to have been good, and the design mistakes that cost us; the things that we are happy with in the end, and the frustrating aspects we wish we had handled better.

Subject Classification

Keywords
  • static type systems
  • side effects
  • aliasing
  • ownership

Metrics

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

References

  1. Thibaut Balabonski and François Pottier. A Coq formalization of itMeåisebox-.1exz\hspace-.3exåisebox.2exz\hspace-.1exo , take 2, July 2014. URL: http://gallium.inria.fr/~fpottier/mezzo/mezzo-coq.tar.gz.
  2. Thibaut Balabonski, François Pottier, and Jonathan Protzenko. The design and formalization of Mezzo, a permission-based programming language. Submitted for publication, July 2014. Google Scholar
  3. Thibaut Balabonski, François Pottier, and Jonathan Protzenko. The design and formalization of Mezzo, a permission-based programming language. Submitted for publication, July 2014. Google Scholar
  4. Thibaut Balabonski, François Pottier, and Jonathan Protzenko. Type soundness and race freedom for Mezzo. In Proceedings of the 12th International Symposium on Functional and Logic Programming (FLOPS 2014), volume 8475 of Lecture Notes in Computer Science, pages 253-269. Springer, 2014. Google Scholar
  5. Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn. Smallfoot: Modular automatic assertion checking with separation logic. In Formal Methods for Components and Objects, volume 4111 of Lecture Notes in Computer Science, pages 115-137. Springer, 2005. Google Scholar
  6. Kevin Bierhoff and Jonathan Aldrich. Modular typestate checking of aliased objects. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 301-320, 2007. Google Scholar
  7. Arthur Charguéraud and François Pottier. Functional translation of a calculus of capabilities. In International Conference on Functional Programming (ICFP), pages 213-224, 2008. Google Scholar
  8. Benjamin Delaware, Bruno C. d. S. Oliveira, and Tom Schrijvers. Meta-theory à la carte. In Principles of Programming Languages (POPL), pages 207-218, 2013. Google Scholar
  9. Armaël Guéneau, François Pottier, and Jonathan Protzenko. The ins and outs of iteration in Mezzo. Higher-Order Programming and Effects (HOPE), 2013. URL: http://goo.gl/NrgKc4.
  10. Cliff B Jones. Specification and design of (parallel) programs. In IFIP congress, volume 83, pages 321-332, 1983. Google Scholar
  11. Niko Matsakis. Focusing on ownership, 2014. Google Scholar
  12. François Pottier. Syntactic soundness proof of a type-and-capability system with hidden state. Journal of Functional Programming, 23(1):38-144, 2013. Google Scholar
  13. François Pottier. Type soundness for Core Mezzo. Unpublished, January 2013. Google Scholar
  14. François Pottier and Jonathan Protzenko. itMeåisebox-.1exz\hspace-.3exåisebox.2exz\hspace-.1exo . http://protz.github.io/mezzo/, July 2014.
  15. Jonathan Protzenko. Mezzo: a typed language for safe effectful concurrent programs. PhD thesis, Université Paris Diderot-Paris 7, 2014. Google Scholar
  16. Jonathan Protzenko. itMeåisebox-.1exz\hspace-.3exåisebox.2exz\hspace-.1exo -web: try itMeåisebox-.1exz\hspace-.3exåisebox.2exz\hspace-.1exo in your browser, 2014. Google Scholar
  17. John C. Reynolds. Separation logic: A logic for shared mutable data structures. In Logic in Computer Science (LICS), pages 55-74, 2002. Google Scholar
  18. Frederick Smith, David Walker, and Greg Morrisett. Alias types. In European Symposium on Programming (ESOP), volume 1782 of Lecture Notes in Computer Science, pages 366-381. Springer, 2000. Google Scholar
  19. Nikhil Swamy, Michael Hicks, Greg Morrisett, Dan Grossman, and Trevor Jim. Safe manual memory management in Cyclone. Science of Computer Programming, 62(2):122-144, 2006. 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 About DROPS Imprint Privacy Contact