Type-and-scope safe programs and their proofs (CPP 2017) - POPL 2017

Sun 15 - Sat 21 January 2017

Who

Guillaume Allais, James Chapman, Conor McBride, James McKinna

Track

Time Zone

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

Use conference time zone: (GMT+01: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

When

Tue 17 Jan 2017 16:00 - 16:30 at Auditorium - Formal verification of programming language foundations

Guillaume Allais

Radboud University Nijmegen

France

James Chapman

Conor McBride

James McKinna

University of Edinburgh

Time Zone

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

Use conference time zone: (GMT+01: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

Session Program

Tue 17 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

	16:00 - 17:30	Formal verification of programming language foundationsCPP at Auditorium

	16:00 30m Talk		Type-and-scope safe programs and their proofs CPP Guillaume Allais Radboud University Nijmegen, James Chapman , Conor McBride , James McKinna University of Edinburgh
	16:30 30m Talk		Formally verified differential dynamic logic CPP Brandon Bohrer , Vincent Rahli SnT, Ivana Vukotic , Marcus Voelp , André Platzer
	17:00 30m Talk		Equivalence of System F and λ2 in Coq based on context morphism lemmas CPP Jonas Kaiser , Tobias Tebbi , Gert Smolka Saarland University