logo

Home    Workshop Program    Important Dates    Program Committee    Call for papers   

Workshop on Partiality and Recursion in Interactive Theorem Provers

15 July 2010, Edinburgh

PAR-10 Program:

Invited Speakers:

Alexander Krauss (Technische Universitat Muenchen) Recursive Definitions of Monadic Functions.

Conor McBride (University of Strathclyde) Djinn, monotonic.

Contributed Talks:

  1. Andreas Abel. Integrating Sized and Dependent Types.
  2. Nils Anders Danielsson. Beating the Productivity Checker Using Embedded Languages.
  3. Issam Maamria and Michael Butler. Rewriting and Well-Definedness within a Proof System.
  4. Claudio Sacerdoti Coen and Silvio Valentini. General recursion and formal topology.
  5. Aaron Stump, Vilhelm Sjöberg and Stephanie Weirich. Termination Casts: A Flexible Approach to Termination with General Recursion.

Informal presentations:

  1. Thorsten Altenkirch and Nils Anders Danielsson. Termination Checking Nested Inductive and Coinductive Types.
  2. Gavin Mendel-Gleason and Geoff Hamilton. Inhabitation of (Co)-inductive Types using Transition Systems.
  3. Tarmo Uustalu. Antifounded coinduction in type theory.

Tentative schedule:

9.00-10.00 Invited Speaker 1.
  • Alexander Krauss. Recursive Definitions of Monadic Functions.
10:00-10:30 Coffee break.
10:30-12:30 Session 1.
  • Andreas Abel. Integrating Sized and Dependent Types.
  • Thorsten Altenkirch and Nils Anders Danielsson. Termination Checking Nested Inductive and Coinductive Types.
  • Nils Anders Danielsson. Beating the Productivity Checker Using Embedded Languages.
  • Tarmo Uustalu. Antifounded coinduction in type theory.
12:30- 14.00 Lunch.
14.00 - 15.00 Invited speaker 2.
  • Conor McBride. Djinn, monotonic.
15.00 - 15.30 Coffee break.
15.30 - 17.30 Session 2.
  • Claudio Sacerdoti Coen and Silvio Valentini. General recursion and formal topology.
  • Aaron Stump, Vilhelm Sjoberg and Stephanie Weirich. Termination Casts: A Flexible Approach to Termination with General Recursion.
  • Issam Maamria and Michael Butler. Rewriting and Well-Definedness within a Proof System.
  • Gavin Mendel-Gleason and Geoff Hamilton. Inhabitation of (Co)-inductive Types using Transition Systems.