Dafny vs. Dala: Experience with Mechanising Language Design (FTfJP 2024)

Mon 16 - Fri 20 September 2024 Vienna, Austria

Who

James Noble, Julian Mackay, Tobias Wrigstad, Andrew Fawcett, Michael Homer

Track

FTfJP 2024

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

Fri 20 Sep 2024 16:30 - 17:00 at EI 2 Pichelmayer - FTfJP Session 3 Chair(s): Dara MacConville

Abstract

Dala is a design for a concurrent dynamic object-oriented language. A key goal of Dala’s design is to avoid data races, by ensuring threads do not share mutable state. In this paper we discuss our experience using the program verification tool Dafny to validate Dafny’s design. We explain how we modelled salient features of Dala in Dafny, and how Dafny did (or did not) assist our confidence in Dala’s design.

File attachments

Dafny vs. Dala: Experience with Mechanising Language Design (paper.pdf)	258KiB

James Noble

Independent. Wellington, NZ

New Zealand

Julian Mackay

Victoria University of Wellington

New Zealand

Tobias Wrigstad

Uppsala University

Sweden

Andrew Fawcett

Victoria University of Wellington

New Zealand

Michael Homer

Victoria University of Wellington

New Zealand

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

Display full programSpecify a time band

Save

Session Program

Fri 20 Sep
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

15:30 - 17:30	FTfJP Session 3FTfJP at EI 2 Pichelmayer Chair(s): Dara MacConville Maynooth University

15:30 30m Talk		Disjoint Polymorphism with Intersection and Union Types FTfJP Baber Rehman University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
16:00 30m Talk		Coeffects for MiniJava: Cf-Mj FTfJP Paola Giannini University of Eastern Piedmont, Giulio Duso University of Eastern Piedmont
16:30 30m Talk		Dafny vs. Dala: Experience with Mechanising Language Design FTfJP James Noble Independent. Wellington, NZ, Julian Mackay Victoria University of Wellington, Tobias Wrigstad Uppsala University, Andrew Fawcett Victoria University of Wellington, Michael Homer Victoria University of Wellington File Attached
17:00 30m Talk		Incrementalizing Polynomial Functors FTfJP Timon Böhler Technical University of Darmstadt, David Richter Technical University of Darmstadt, Mira Mezini TU Darmstadt; hessian.AI; National Research Center for Applied Cybersecurity ATHENE

Information for Participants

Fri 20 Sep 2024 15:30 - 17:30 at EI 2 Pichelmayer - FTfJP Session 3 Chair(s): Dara MacConville

Info for room EI 2 Pichelmayer:

Map: https://tuw-maps.tuwien.ac.at/?q=CF0235

Room tech: https://raumkatalog.tiss.tuwien.ac.at/room/15717