seminars
Detail
Publication date: 4 de March, 2026Coma: an intermediate verification language with explicit abstraction barriers
Coma is a formally defined intermediate verification language. It adopts the continuation-passing style which allows us to express in a natural manner the standard control structures—conditionals, loops, subroutine calls, and exception handling—using only three elementary constructions.
A special programming construct representing the abstraction barrier allows the programmer to decide which part of a function implementation is visible to (and verified by) the caller, and which part is hidden from the caller and verified at the definition site. This offers us an additional degree of freedom, as we can provide separate specification (or none at all) for different execution paths.
A special programming construct representing the abstraction barrier allows the programmer to decide which part of a function implementation is visible to (and verified by) the caller, and which part is hidden from the caller and verified at the definition site. This offers us an additional degree of freedom, as we can provide separate specification (or none at all) for different execution paths.
Paper presented at ESOP 2025: https://doi.org/10.1007/
| URL | https://meet.google.com/bzb-aqiv-zem |
|---|---|
| Date | 18/03/2026 2:00 pm |
| Location | DI Seminars Room and Google Meet |
| Host Bio | Paul Patault is a PhD candidate in computer science at Université Paris-Saclay and a member of the Laboratoire Méthodes Formelles (LMF). He is supervised by Jean-Christophe Filliâtre and Andrei Paskevich. His research focuses on Coma, an intermediate language for deductive program verification. In particular, he works on a formally verified implementation of Coma in Rocq. |