coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] PAR-10 call for participation

From: Ekaterina Komendantskaya <komendantskaya AT gmail.com>
To: coq-club AT inria.fr, lfcs-interest AT dcs.ed.ac.uk, stp AT macs.hw.ac.uk, SPLS <SPLS AT dcs.gla.ac.uk>, blc AT cs.nott.ac.uk, functional-programming AT cs.st-and.ac.uk, hamming-members AT inf.ed.ac.uk, categories AT mta.ca
Subject: [Coq-Club] PAR-10 call for participation
Date: Tue, 4 May 2010 10:01:23 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:from:date:message-id:subject:to:content-type :content-transfer-encoding; b=ErS5SbFkrGFsHLpiTBiMH/8zD2TCWm9B4ovuC/NAyFUVmykXIxX9VP4988L/I6wO3V fEZG3foGOBnNPeaQNoO+1c3sr6TLwl4LLTW6q7PDhlcwDwhLZseR7lJ6lVCYGNnF8rvu HpEC/BT1rb8Rke/MQGr/snevQW2rWERzZ9DTQ=

========================================================================
                      Call for Participation

                           PAR 2010

Workshop on Partiality And Recursion in Interactive Theorem Provers
                  Edinburgh, UK, 15 July 2010
                (satellite workshop of ITP'10)
                   a mid-FLoC 2010 workshop

           <http://www.cs.st-andrews.ac.uk/~ek/PAR-10/>

========================================================================

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
details.

Registration is now open via FLoC 2010 registration form
<http://www.floc-conference.org/registration.html>
Early registration is open until May 17th.

The programme of the workshop will comprise:

Invited Speakers:
1. Alexander Krauss (Technische Universitat Muenchen): Recursive
  Definitions of Monadic Functions.
2. 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.

See also the workshop program at
<http://www.cs.st-andrews.ac.uk/~ek/PAR-10/program.html>

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

[Coq-Club] PAR-10 call for participation, Ekaterina Komendantskaya