TTT : Type Theory Based Tools
[We have funding possibilities for students and young researchers, see below. Note the early deadline.]
Overview
The aim of this workshop is to showcase modern tools based on type theory, whether designed for programming or for verification, whether academic projects or used in an industrial setting. It will provide a forum to highlight and discuss their common and their distinctive features, and the future directions of development of the tools. The program will consist of invited and contributed talks, and will encourage informal discussion. Abstracts will be displayed on the website of the workshop but there will be no proceedings. We solicit abstract submissions proposing demos, case studies, describing the impact of a theoretical result on practice, or any other aspect of the development and use of tools based on type theory. In particular, we welcome submissions about prototype implementations and promising work in progress, as soon as they have the potential of raising interesting discussions.
This workshop is funded by the EUTypes COST project. The program will include a plenary discussion on the role of the EUTypes project in the community and planning of activities for 2017.
Invited Speakers
- Robbert Krebbers, Delft University of Technology, Netherlands
- Aaron Tomb, Galois, US
- Anders Mörtberg, Inria, France
Registration
Registration information will be soon available at the main POPL 2017 website: http://conf.researchr.org/home/POPL-2017
Participant funding
The EUTypes COST project can fund students and young researchers from countries participating in the project to attend the workshop – check this page to see if your country is listed. The application should include the following information:
- Your name
- Your institution
- The name of your supervisor(s)
- The url of your webpage if you have one
- Your research topics or interests in 1 paragraph
and should be sent to ttt2017@easychair.org as soon as possible and no later than November 20th.
Contact
For any query about this workshop, please contact us at ttt2017@easychair.org
Accepted Papers
Call for Abstracts
Submissions for talks and demonstrations should be described in an extended abstract, between 1 and 2 pages in length. We suggest formatting the text using the two-column SIGPLAN LaTex style (9pt font).
Submission page: https://easychair.org/conferences/?conf=ttt2017
Important dates
- Submission deadline: November 30th (AoE)
- Notification: December 15th
- Workshop: January 15th
Sun 15 JanDisplayed 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 |