Transferring Arithmetic Decision Procedures (on Z) to Alternative Representations (CoqPL 2017 - The Third International Workshop on Coq for Programming Languages)

Sun 15 - Sat 21 January 2017

Track

CoqPL 2017

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

Save

When

Sat 21 Jan 2017 17:40 - 18:05 at Auditorium - Afternoon Session Chair(s): Matthieu Sozeau

File attachments

Abstract (CoqPL_2017_paper_7.pdf)	140KiB

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

Display full programSpecify a time band

Save

Session Program

Sat 21 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 18:05	Afternoon SessionCoqPL at Auditorium Chair(s): Matthieu SozeauInria

16:00 25m Talk		Synthetic topology in HoTT for probabilistic programming CoqPL Florian Faissole, Bas Spitters File Attached
16:25 25m Talk		CertiCoq: A verified compiler for Coq CoqPL Abhishek Anand, Andrew AppelPrinceton, Greg MorrisettCornell University, Zoe ParaskevopoulouPrinceton University, USA, Randy PollackHarvard University, Olivier Savary BelangerPrinceton University, Matthieu SozeauInria, Matthew WeaverPrinceton University File Attached
16:50 25m Talk		CertSkel: a Verified Compiler for a Coq-embedded GPGPU DSL CoqPL Izumi AsakuraTokyo Institute of Technology, Japan, Hidehiko MasuharaTokyo Institute of Technology, Tomoyuki AotaniTokyo Institute of Technology File Attached
17:15 25m Talk		Verification of Implementations of Distributed Systems Under Churn CoqPL Ryan DoengesUniversity of Washington, James R. WilcoxUniversity of Washington, Doug WoosUniversity of Washington, Zachary TatlockUniversity of Washington, Seattle, Karl Palmskog File Attached
17:40 25m Talk		Transferring Arithmetic Decision Procedures (on Z) to Alternative Representations CoqPL Nicolas Magaud File Attached

Transferring Arithmetic Decision Procedures (on Z) to Alternative Representations

Sat 21 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Nicolas Magaud

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposiums

Transferring Arithmetic Decision Procedures (on Z) to Alternative Representations

Program Display Configuration

Program Display Configuration

Sat 21 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Nicolas Magaud

Sat 21 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change