Reasoning about Effect Parametricity Using Dependent Types (TyDe 2019)

Write a Blog >>

Sun 18 - Fri 23 August 2019 Berlin, Germany

Who

Joris Ceulemans, Andreas Nuyts, Dominique Devriese

Track

TyDe 2019

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

Sun 18 Aug 2019 17:10 - 17:30 at Aurora Borealis - Effects Chair(s): David Darais

Abstract

In this extended abstract, we will describe how properties involving effect parametricity can be proved in ParamDTT, a dependent type system with support for parametricity.

Link to Preprint

http://tydeworkshop.org/2019-abstracts/paper11.pdf

Joris Ceulemans

KU Leuven

Belgium

Andreas Nuyts

KU Leuven, Belgium

Belgium

Dominique Devriese

Vrije Universiteit Brussel

Belgium

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

Sun 18 Aug
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

17:10 - 18:10	EffectsTyDe at Aurora Borealis Chair(s): David Darais University of Vermont

17:10 20m Talk		Reasoning about Effect Parametricity Using Dependent Types TyDe Joris Ceulemans KU Leuven, Andreas Nuyts KU Leuven, Belgium, Dominique Devriese Vrije Universiteit Brussel Pre-print
17:30 20m Talk		How to do proofs? Practically proving properties about effectful programs' results (functional pearl) TyDe Koen Jacobs KU Leuven, Andreas Nuyts KU Leuven, Belgium, Dominique Devriese Vrije Universiteit Brussel Link to publication