Formalizing Simple Refinements in Coq (CoqPL 2016) - POPL 2016

Write a Blog >>

Wed 20 - Sat 23 January 2016 St. Petersburg, Florida, United States

Who

Nicolás Lehmann, Éric Tanter

Track

Time Zone

The program is currently displayed in (GMT-05:00) Guadalajara, Mexico City, Monterrey.

Use conference time zone: (GMT-05:00) Guadalajara, Mexico City, MonterreySelect 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

Sat 23 Jan 2016 11:20 - 11:45 at Room St Petersburg III - Session II

Link to Publication

http://arthur.chargueraud.org/events/coqpl2016/CoqPL_2016_paper_9.pdf

Nicolás Lehmann

Éric Tanter

University of Chile, Chile

Chile

Time Zone

The program is currently displayed in (GMT-05:00) Guadalajara, Mexico City, Monterrey.

Use conference time zone: (GMT-05:00) Guadalajara, Mexico City, MonterreySelect 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

Sat 23 Jan
Displayed time zone: Guadalajara, Mexico City, Monterrey change

	10:30 - 12:05	Session IICoqPL at Room St Petersburg III

	10:30 25m Talk		A Coq Library for Binary Logical Relations CoqPL Jérémie Koenig Link to publication
	10:55 25m Talk		A Coinduction Proof Rule for Hoare Doubles CoqPL Christian J. Bell MIT CSAIL Link to publication
	11:20 25m Talk		Formalizing Simple Refinements in Coq CoqPL Nicolás Lehmann , Éric Tanter University of Chile, Chile Link to publication
	11:45 20m Talk		Company-Coq: Taking Proof General one step closer to a real IDE CoqPL Clément Pit-Claudel MIT CSAIL, Pierre Courtieu Link to publication