[TYPES/announce] Call for Participation: 2007 Workshop on ML
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Below is the preliminary program for the 2007 Workshop on ML, which is co-located with ICFP 2007 and will take place on Friday, October 5. The early registration deadline is this Friday, September 7! We are pleased to have Didier Rémy as our invited speaker. In addition, we are planning to conclude the workshop with a 5-Minute Madness session, in which attendees can give brief impromptu talks on ML-related topics. The proposed theme for this year's madness session is Design Ideas for Next-Generation ML, but talks on other topics are welcome as well. If you are interested in giving a 5-Minute Madness talk, please send mail (with a brief mention of what you would like to talk about) to the program chair at [EMAIL PROTECTED] I hope to see you at the workshop! Derek Dreyer -- ML 2007 Website: http://research.microsoft.com/~crusso/ml2007/ Registration Website: http://proglang.informatik.uni-freiburg.de/ICFP2007/registration.shtml Preliminary Program: 8:50-9:00 Welcome/Opening remarks Derek Dreyer, Program Chair 9:00-10:00 Invited talk: MLF for Everyone (Users, Implementers, and Designers) Didier Rémy 10:00-10:30 Coffee Break 10:30-12:30 Efficient ML Type Inference Using Ranked Type Variables George Kuan and David MacQueen Status Report: The Manticore Project Matthew Fluet, Nic Ford, Mike Rainey, John Reppy, Adam Shaw and Yingqi Xiao Status Report: HOT Pickles, and How to Serve Them Andreas Rossberg, Guido Tack and Leif Kornstaedt A Persistent Union-Find Data Structure Sylvain Conchon and Jean-Christophe Filliatre 12:30-14:00 Lunch Break 14:00-15:30 Status Report: Specifying JavaScript with ML David Herman and Cormac Flanagan Status Report: Layered Streaming XML Processing with Modules Tyng-Ruey Chuang and Max Schaefer Status Report: Marionnet -- How to Implement a Virtual Network Laboratory in Six Months and Be Happy Jean-Vincent Loddo and Luca Saiu 15:30-16:00 Coffee Break 16:00-17:00 Generics for the Working ML'er Vesa Karvonen Practical Generic Programming in OCaml Jeremy Yallop 17:00-18:00 5-Minute Madness: Design Ideas for Next-Generation ML
[TYPES/announce] 14 month position Imperial College London
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] We have a 14 month position at Imperial College to work on the EU project MOBIUS. We will be working on the use of type systems to support modular verification. The text for the ad, and application form can be be found at http://www.jobs.ac.uk/jobs/CG894/Research_Assistant_Research_Associate/ I am happy to discuss any further questions. Sophia Drossopoulou
[TYPES/announce] Call for Participation: PLPV 2007
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Programming Languages meets Program Verification (PLPV) 2007 Affiliated with ICFP 2007 Freiburg, Germany Topic: PLPV is concerned with language-based approaches to program verification. These approaches integrate programming language semantics and verification techniques in a tighter way than is typically done in traditional verification. An example is dependently typed programming, where types provide rich specifications, and programs may contain proof terms to establish type equivalences or satisfy pre-conditions. The motivation for this approach is to reduce the burden of program verification by taking greater advantage of semantic properties (like type properties) of the program during verification. Schedule, October 5th: 09:00-10:00Invited Talk (Chair: Hongwei Xi) Jessie: an Intermediate Language for Java and C Verification. Claude Marché. 10:30-12:00Session I: Monads, Refinement (Chair: Stefan Monnier) Compound Monads in Specification Languages. Jeremy Dawson. A Coinductive Monad for Prop-Bounded Recursion. Adam Megacz. Refined typechecking with Stardust. Joshua Dunfield. 14:00-15:30Session II: Low-level Types, Dependence (Chair: Martin Sulzmann) The Swiss Coercion. Stefan Monnier. Implementing Reliable Linux Device Drivers in ATS. Rui Shi. Pattern matching coverage checking with dependent types using set approximations. Nicolas Oury. 16:00-15:15Session III: Equality, Panel (Chair: Aaron Stump) Observational Equality, Now! Thorsten Altenkirch, Conor McBride and Wouter Swierstra. Panel discussion For more information: www.plpv.org
