[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS] PAR'10: Programme and Call for Participation
Call for Participation
Workshop on Partiality And Recursion in Interactive Theorem Provers
Edinburgh, UK, 15 July 2010
(satellite workshop of ITP'10)
a mid-FLoC 2010 workshop
PAR'10 is a one-day workshop organised as a part of FLoC'10. It is a
venue for researchers working on new approaches to cope with partial
functions and terminating general recursion in (interactive) theorem
provers. See <http://www.cs.st-andrews.ac.uk/~ek/PAR-10/> for further
Registration is now open via FLoC 2010 registration form
Early registration is open until May 17th.
The programme of the workshop will comprise:
1. Alexander Krauss (Technische Universitat Muenchen): Recursive
Definitions of Monadic Functions.
2. Conor McBride (University of Strathclyde): Djinn, monotonic.
1. Andreas Abel: Integrating Sized and Dependent Types.
2. Nils Anders Danielsson: Beating the Productivity Checker Using
3. Issam Maamria and Michael Butler: Rewriting and Well-Definedness
within a Proof System.
4. Claudio Sacerdoti Coen and Silvio Valentini: General Recursion and
5. Aaron Stump, Vilhelm Sj÷berg and Stephanie Weirich: Termination
Casts: A Flexible Approach to Termination with General Recursion.
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.
See also the workshop program at
At PAR'10, we envisage an open, friendly, and inspiring discussion of the
latest trends and achievements in the area.
Looking forward to seeing you in Edinburgh,
-- PAR'10 organising committee