A Coq-based synthesis of Scala programs which are correct-by-construction (FTfJP 2017 - (Formal Techniques for Java-like Programs))

Write a Blog >>

Sun 18 - Fri 23 June 2017 Barcelona, Spain

co-located with PLDI, ECOOP, Curry On, DEBS, LCTES and ISMM

Who

Youssef El Bakouny, Tristan Crolard, Dani Mezher

Track

FTfJP 2017

Time Zone

The program is currently displayed in (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna.

Use conference time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, ViennaSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

Tue 20 Jun 2017 11:00 - 11:20 at Vertex WS217 - B Chair(s): Santosh Nagarakatte

Abstract

The present paper introduces Scala-of-Coq, a new compiler that allows a Coq-based synthesis of Scala programs which are ``correct-by-construction''. A typical workflow features a user implementing a Coq functional program, proving this program’s correctness with regards to its specification and making use of Scala-of-Coq to synthesize a Scala program that can seamlessly be integrated into an existing industrial Scala or Java application.

Link to Preprint

https://arxiv.org/abs/1706.05271

Youssef El Bakouny

CIMTI - ESIB - Saint-Joseph University - Beirut, Lebanon

Lebanon

Tristan Crolard

CEDRIC - CNAM - Paris, France

Dani Mezher