POPL 2017 (series) / TTT 2017 (series) /
TTT 2017 Program
This is the TTT 2017 program - see the full program for POPL 2017 and all affiliated events.
Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Sun 15 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Sun 15 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
08:50 - 10:00 | |||
08:50 10mDay opening | Welcome TTT | ||
09:00 20mTalk | A Case Study in Programming Coinductive Proofs in Beluga: Howe's Method TTT | ||
09:20 20mTalk | Needle & Knot: A Framework for Meta-Theoretical Specifications with Binding TTT | ||
09:40 20mTalk | Equivalence of System F and λ2 in Abella TTT |
10:30 - 12:00 | |||
10:30 50mTalk | Invited Talk -- Type Theory in the Software Analysis Workbench TTT Aaron Tomb Galois, Inc. | ||
11:20 20mTalk | Modelling Program Behaviour within Software Verification Tool LAV TTT | ||
11:40 20mTalk | agdARGS - Declarative Hierarchical Command Line Interfaces TTT Guillaume Allais Radboud University Nijmegen |
14:00 - 15:30 | |||
14:00 50mTalk | Invited Talk -- Cubical Type Theory: a constructive interpretation of the univalence axiom TTT Anders Mörtberg Inria | ||
14:50 20mTalk | Equations: a tool for dependent pattern-matching TTT File Attached | ||
15:10 20mTalk | Coq's Prolog and application to defining semi-automatic tactics TTT File Attached |
16:00 - 18:00 | |||
16:00 50mTalk | Invited Talk -- Iris: a framework for higher-order concurrent separation logic in Coq TTT Robbert Krebbers Delft University of Technology, Netherlands | ||
16:50 20mTalk | Introducing MetaCoq: A Safe Tactic Language for Coq TTT Beta Ziliani FAMAF, UNC (Argentina) / CONICET (Argentina) | ||
17:10 50mOther | COST EUTypes session TTT |