Program - POPL 2017

Detailed Table Session Timeline Detailed Timeline

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

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

Sun 15 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

08:50 - 10:00	First Morning SessionTTT at Salle 105, Barre 44-54 Chair(s): Assia Mahboubi INRIA

08:50 10m Day opening		Welcome TTT
09:00 20m Talk		A Case Study in Programming Coinductive Proofs in Beluga: Howe's Method TTT David Thibodeau McGill University, Canada, Alberto Momigliano , Brigitte Pientka McGill University
09:20 20m Talk		Needle & Knot: A Framework for Meta-Theoretical Specifications with Binding TTT Steven Keuchel , Koar Marntirosian , Tom Schrijvers KU Leuven
09:40 20m Talk		Equivalence of System F and λ2 in Abella TTT Jonas Kaiser , Gert Smolka Saarland University

10:30 - 12:00	Second Morning SessionTTT at Salle 105, Barre 44-54 Chair(s): Keiko Nakata

10:30 50m Talk		Invited Talk -- Type Theory in the Software Analysis Workbench TTT Aaron Tomb Galois, Inc.
11:20 20m Talk		Modelling Program Behaviour within Software Verification Tool LAV TTT Milena Vujosevic Janicic
11:40 20m Talk		agdARGS - Declarative Hierarchical Command Line Interfaces TTT Guillaume Allais Radboud University Nijmegen

14:00 - 15:30	First Afternoon SessionTTT at Salle 105, Barre 44-54 Chair(s): Bas Spitters

14:00 50m Talk		Invited Talk -- Cubical Type Theory: a constructive interpretation of the univalence axiom TTT Anders Mörtberg Inria
14:50 20m Talk		Equations: a tool for dependent pattern-matching TTT Cyprien Mangin , Matthieu Sozeau Inria File Attached
15:10 20m Talk		Coq's Prolog and application to defining semi-automatic tactics TTT Théo Zimmermann IRIF, Université Paris Diderot, Hugo Herbelin File Attached

16:00 - 18:00	Second Afternoon SessionTTT at Salle 105, Barre 44-54 Chair(s): Hugo Herbelin

16:00 50m Talk		Invited Talk -- Iris: a framework for higher-order concurrent separation logic in Coq TTT Robbert Krebbers Delft University of Technology, Netherlands
16:50 20m Talk		Introducing MetaCoq: A Safe Tactic Language for Coq TTT Beta Ziliani FAMAF, UNC (Argentina) / CONICET (Argentina)
17:10 50m Other		COST EUTypes session TTT

TTT 2017 Program

Sun 15 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposia

TTT 2017 Program

Switch Program View

Program Display Configuration

Sun 15 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Get Calendar (iCal)

Sun 15 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change