Program - CPP 2016

POPL 2016 (series) / CPP 2016 (series) /

CPP 2016 Program

This is the CPP 2016 program - see the full program for POPL 2016 and all affiliated events.

Detailed Table Session Timeline Detailed Timeline

Switch Program View

You're viewing a filtered program.

Do you want to keep these filters active in the new view?

Get Calendar (iCal)

Filter Program | active: Mon 18 Jan 2016

Dates

Mon 18 Jan 2016

Tue 19 Jan 2016

Rooms

Room St Petersburg II

Tracks

CPP

Badges

Nothing to filter

Your Program

Nothing to filter

Program Display Configuration

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

Save

You're viewing the program in a time zone which is different from your device's time zone change time zone

Mon 18 Jan
Displayed time zone: Guadalajara, Mexico City, Monterrey change

09:00 - 10:00	Session 1: Invited talk by Harvey FriedmanCPP at Room St Petersburg II

09:00 60m Talk		Perspectives on Formal Verfication CPP Harvey Friedman Ohio State University

10:30 - 12:00	Session 2: Verifying Imperative ProgramsCPP at Room St Petersburg II

10:30 30m Talk		Higher-order Representation Predicates in Separation Logic CPP Arthur Charguéraud
11:00 30m Talk		A Unified Coq Framework for Verifying C Programs with Floating-Point Computations CPP Tahina Ramananandro , Paul Mountcastle , Benoit Meister , Richard Lethin
11:30 30m Talk		Refinement Based Verification of Imperative Data Structures CPP Peter Lammich Technische Universität München

14:00 - 15:30	Session 3: Design and Implementation of Theorem ProversCPP at Room St Petersburg II

14:00 30m Talk		The Vampire and the FOOL CPP Evgenii Kotelnikov Chalmers University of Technology, Laura Kovacs Chalmers University of Technology, Giles Reger University of Manchester, Andrei Voronkov University of Manchester
14:30 30m Talk		Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions CPP Lukasz Czajka University of Innsbruck
15:00 30m Talk		Mizar Environment for Isabelle CPP Cezary Kaliszyk University of Innsbruck, Karol Pąk University of Bialystok, Institute of Computer Science, Josef Urban

16:00 - 18:00	Session 4: MathematicsCPP at Room St Petersburg II

16:00 30m Talk		A Modular, Efficient Formalisation of Real Algebraic Numbers CPP Wenda Li University of Cambridge, Lawrence Paulson Cambridge University
16:30 30m Talk		Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials CPP Sophie Bernard INRIA, Yves Bertot INRIA, Laurence Rideau INRIA, Pierre-Yves Strub IMDEA Software Institute
17:00 30m Talk		Formalizing Jordan Normal Forms in Isabelle/HOL CPP René Thiemann University of Innsbruck, Akihisa Yamada
17:30 30m Talk		Formalization of a Newton series representation of polynomials CPP Cyril Cohen , Boris Djalal INRIA

Tue 19 Jan
Displayed time zone: Guadalajara, Mexico City, Monterrey change

09:00 - 10:00	Session 5: Invited talk by Leonardo de MouraCPP at Room St Petersburg II

09:00 60m Talk		Dependent Type Practice CPP Leonardo de Moura Microsoft Research, Redmond

10:30 - 12:00	Session 6: FoundationsCPP at Room St Petersburg II

10:30 30m Talk		A Logic of Proofs for Differential Dynamic Logic CPP Nathan Fulton Carnegie Mellon University, André Platzer
11:00 30m Talk		Constructing the Propositional Truncation using Non-recursive HITs CPP Floris van Doorn Carnegie Mellon University
11:30 30m Talk		A Nominal Exploration of Intuitionism CPP Vincent Rahli SnT, Mark Bickford Cornell University

14:00 - 15:30	Session 7: Verification for Concurrent and Distributed SystemsCPP at Room St Petersburg II

14:00 30m Talk		Bisimulation Up-to Techniques for Psi-calculi CPP Johannes Å. Pohjola Uppsala University, Joachim Parrow Uppsala University
14:30 30m Talk		Planning for Change in a Formal Verification of the Raft Consensus Protocol CPP Doug Woos University of Washington, James R. Wilcox University of Washington, Steve Anton University of Washington, Zachary Tatlock University of Washington, Seattle, Michael D. Ernst University of Washington, Thomas Anderson University of Washington Pre-print
15:00 30m Talk		A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules CPP Michel St-Martin University of Ottawa, Amy Felty University of Ottawa

16:00 - 17:00	Session 8: Compiler VerificationCPP at Room St Petersburg II

16:00 30m Talk		Formal Verification of Control-flow Graph Flattening CPP Sandrine Blazy IRISA / University of Rennes 1, Alix Trieu ENS Rennes
16:30 30m Talk		Axiomatic Semantics for Compiler Verification CPP Steven Schäfer , Sigurd Schneider Saarland University, Gert Smolka Saarland University

18:00 - 21:00	CPP Reception, sponsored by the DeepSpec projectCPP at Room St Petersburg I

18:00 3h Social Event		CPP Reception, sponsored by the DeepSpec project CPP

Get Calendar (iCal)

iCalendar subscription service for your personal schedule

You first need to have starred events () in order to use the iCalendar subscription service.

Currently Viewed Program

Downloads the currently viewed program (with filters applied) in iCal format

Session Calendar (ical)

session-calendar.ics

Detailed Event Calendar (ical)

event-calendar.ics

xMon 14 Jul 17:14

CPP 2016 Program

Switch Program View

Program Display Configuration

Mon 18 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change

Tue 19 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change

Get Calendar (iCal)

Mon 18 Jan
Displayed time zone: Guadalajara, Mexico City, Monterrey change

Tue 19 Jan
Displayed time zone: Guadalajara, Mexico City, Monterrey change