A Coq Formal Proof of the Lax–Milgram theorem (CPP 2017) - POPL 2017

Sun 15 - Sat 21 January 2017

Who

Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero

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

Mon 16 Jan 2017 16:00 - 16:30 at Auditorium - Formalized mathematics with numerical computations

Sylvie Boldo

François Clément

Florian Faissole

Vincent Martin

Micaela Mayero

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

Mon 16 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

	16:00 - 18:00	Formalized mathematics with numerical computationsCPP at Auditorium

	16:00 30m Talk		A Coq Formal Proof of the Lax–Milgram theorem CPP Sylvie Boldo , François Clément , Florian Faissole , Vincent Martin , Micaela Mayero
	16:30 30m Talk		A Reflexive Tactic for Polynomial Positivity using Numerical Solvers and Floating-Point Computations CPP Erik Martin-Dorel IRIT, Université Paul Sabatier, Pierre Roux
	17:00 30m Talk		Markov Processes in Isabelle/HOL CPP Johannes Hölzl Technische Universität München DOI Pre-print File Attached
	17:30 30m Talk		Formalising Real Numbers in Homotopy Type Theory CPP Gaetan Gilbert