A Case Study in Programming Coinductive Proofs in Beluga: Howe's Method (TTT 2017) - POPL 2017

Sun 15 - Sat 21 January 2017

Who

David Thibodeau, Alberto Momigliano, Brigitte Pientka

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

Sun 15 Jan 2017 09:00 - 09:20 at Salle 105, Barre 44-54 - First Morning Session Chair(s): Assia Mahboubi

David Thibodeau

McGill University, Canada

Alberto Momigliano

Brigitte Pientka

McGill University

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

Sun 15 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

	08:50 - 10:00	First Morning SessionTTT at Salle 105, Barre 44-54 Chair(s): Assia Mahboubi INRIA

	08:50 10m Day opening		Welcome TTT
	09:00 20m Talk		A Case Study in Programming Coinductive Proofs in Beluga: Howe's Method TTT David Thibodeau McGill University, Canada, Alberto Momigliano , Brigitte Pientka McGill University
	09:20 20m Talk		Needle & Knot: A Framework for Meta-Theoretical Specifications with Binding TTT Steven Keuchel , Koar Marntirosian , Tom Schrijvers KU Leuven
	09:40 20m Talk		Equivalence of System F and λ2 in Abella TTT Jonas Kaiser , Gert Smolka Saarland University