print · login   

TTT : Type Theory Based Tools

EUTypes WG3-4 meeting / Satellite workshop of POPL 2017, Paris, France, 15 January

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 COST EUTypes project (https://eutypes.cs.ru.nl/). 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

Program, Abstracts, Slides

  • 09:00 - 09:20: A Case Study in Programming Coinductive Proofs in Beluga: Howe's Method. David Thibodeau, Alberto Momigliano, Brigitte Pientka. abstract, slides
  • 09:20 - 09:40: Needle & Knot: A Framework for Meta-Theoretical Specifications with Binding. Steven Keuchel, Klara Mardirosian, Tom Schrijvers. abstract, slides Δ
  • 09:40 - 10:00: Equivalence of System F in Coq and Abella. Jonas Kaiser, Gert Smolka. abstract, slides, link to project page
  • Break
  • 10:30 - 11:20: Invited Talk -- Type Theory in the Software Analysis Workbench. Aaron Tomb. slides
  • 11:20 - 11:40: Modelling Program Behaviour within Software Verification Tool LAV. Milena Vujosevic Janicic. abstract, slides
  • 11:40 - 12:00: agdARGS - Declarative Hierarchical Command Line Interfaces. Guillaume Allais. abstract, slides
  • Lunch Break
  • 14:00 - 14:50: Invited Talk -- Cubical Type Theory: a constructive interpretation of the univalence axiom. Anders Mörtberg. slides
  • 14:50 - 15:10: Equations: a tool for dependent pattern-matching. Cyprien Mangin, Matthieu Sozeau. abstract, slides, demo.zip
  • 15:10 - 15:30: Coq's Prolog and application to defining semi-automatic tactics. Théo Zimmermann, Hugo Herbelin. abstract, slides
  • Break
  • 16:00 - 16:50: Invited Talk -- Iris: a framework for higher-order concurrent separation logic in Coq. Robbert Krebbers. slides
  • 16:50 - 17:10: Introducing MetaCoq: A Safe Tactic Language for Coq. Beta Ziliani. abstract, slides
  • 17:10 - 18:00: COST EUTypes session