CPP 2016 - CPP 2016

Topics of interest:

We welcome submissions in research areas related to formal certification of programs and proofs. The following is a suggested list of topics of interest to CPP. This is a non-exhaustive list and should be read as a guideline rather than a requirement.

certified or certifying programming, compilation, linking, OS kernels, runtime systems, and security monitors
program logics, type systems, and semantics for certified code
certified decision procedures, mathematical libraries, and mathematical theorems
proof assistants and proof theory
new languages and tools for certified programming
program analysis, program verification, and proof-carrying code
certified secure protocols and transactions
certificates for decision procedures, including linear algebra, polynomial systems, SAT, SMT, and unification in algebras of interest
certificates for semi-decision procedures, including equality, first-order logic, and higher-order unification
certificates for program termination *logics for certifying concurrent and distributed programs
higher-order logics, logical systems, separation logics, and logics for security
teaching mathematics and computer science with proof assistants

Please see the external CPP web site for the full details.

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

Accepted Papers

	Title
	A Logic of Proofs for Differential Dynamic Logic CPP Nathan Fulton, André Platzer
	A Modular, Efficient Formalisation of Real Algebraic Numbers CPP Wenda Li, Lawrence Paulson
	A Nominal Exploration of Intuitionism CPP Vincent Rahli, Mark Bickford
	A Unified Coq Framework for Verifying C Programs with Floating-Point Computations CPP Tahina Ramananandro, Paul Mountcastle, Benoit Meister, Richard Lethin
	A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules CPP Michel St-Martin, Amy Felty
	Axiomatic Semantics for Compiler Verification CPP Steven Schäfer, Sigurd Schneider, Gert Smolka
	Bisimulation Up-to Techniques for Psi-calculi CPP Johannes Å. Pohjola, Joachim Parrow
	Constructing the Propositional Truncation using Non-recursive HITs CPP Floris van Doorn
	Formalization of a Newton series representation of polynomials CPP Cyril Cohen, Boris Djalal
	Formalizing Jordan Normal Forms in Isabelle/HOL CPP René Thiemann, Akihisa Yamada
	Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials CPP Sophie Bernard, Yves Bertot, Laurence Rideau, Pierre-Yves Strub
	Formal Verification of Control-flow Graph Flattening CPP Sandrine Blazy, Alix Trieu
	Higher-order Representation Predicates in Separation Logic CPP Arthur Charguéraud
	Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions CPP Lukasz Czajka
	Mizar Environment for Isabelle CPP Cezary Kaliszyk, Karol Pąk, Josef Urban
	Planning for Change in a Formal Verification of the Raft Consensus Protocol CPP Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, Thomas Anderson Pre-print
	Refinement Based Verification of Imperative Data Structures CPP Peter Lammich
	The Vampire and the FOOL CPP Evgenii Kotelnikov, Laura Kovacs, Giles Reger, Andrei Voronkov

Call for Papers

Please see the external CPP web site for the full details, but here’s a summary of the most important points.

Abstracts due: October 7
Papers due: October 12
Author Notification: November 18
Final versions due: December 4
Conference: January 18-19

The paper format is compatible with the one from recent POPL and ICFP conferences.

CPP

Topics of interest:

Program Display Configuration

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

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

Accepted Papers

Call for Papers

Jeremy AvigadProgram Co-Chair

Carnegie Mellon University

Sandrine Blazy

IRISA / University of Rennes 1

Adam ChlipalaProgram Co-Chair

MIT

United States

Thierry Coquand

Chalmers University of Technology, Sweden

John Harrison

Intel

Chris Hawblitzel

Microsoft Research

Cătălin Hriţcu

INRIA Paris

France

Brian Huffman

Galois

Laura Kovacs

Chalmers University of Technology

Peter Lammich

Technische Universität München

Hongjin Liang

University of Science and Technology of China

Daniel R. Licata

Wesleyan University

Panagiotis Manolios

Northeastern University

Dale Miller

INRIA Saclay and LIX

Dominic Mulligan

Cambridge University

Lawrence Paulson

Cambridge University

Andrei Popescu

Middlesex University, London

Claudio Sacerdoti Coen

University of Bologna

Zachary Tatlock

University of Washington, Seattle

United States

Cesare Tinelli

University of Iowa

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

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