[Agda] Twelf Tutorial: Second Call for Participation

[Dan Licata]

Dear Agda hackers,

Twelf and Agda have a lot in common (issues such as term
reconstruction/implicit argument inference, coverage of dependent
pattern matching, termination checking), and there may be some
opportunities for cross-pollination if more people become familiar with
both languages.

We're running a Twelf Tutorial at POPL this year, and the early
registration deadline for it (and other POPL events, such as PLPV) is
this week.  We have a very interactive program planned, and we would
appreciate it if you would register soon so we know how many teaching
assistants we'll need.

Thanks! -Dan

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

Tutorial Announcement and Call for Participation

Mechanizing Metatheory with LF and Twelf

Monday 19 January 2008
Savannah, GA
Co-located with POPL 2009

Registration open! (Early registration ends December 19)
http://twelftutorial.plparty.org

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

The Principles of Programming group at Carnegie Mellon University
invites you to a tutorial on the use of LF and Twelf for specifying,
implementing, and proving properties of programming languages.

The tutorial will be a highly interactive introduction to LF and Twelf
aimed at programming languages researchers. No prior experience with LF
and Twelf is assumed. We will concentrate on two topics:

 * Representing programming languages in the LF logical framework
 * Using Twelf to prove properties of those languages

Participants will leave the workshop with experience in reading and
writing LF representations of programming languages, and experience
reading, writing, and debugging Twelf proofs.

You can register for the tutorial when you register for POPL 2009.