< Back to PLI'03
Front Page

PLI'03 Program: Day by day

Sunday | Monday | Tuesday | Wednesday | Thursday | Friday

Sunday 24/8
Welcoming Reception
Monday 25/8
08:45 – 09:00
ICFP and DP-COOL Openings
09.00 – 10.00
ICFP invited talk
  • Conservation of information: Applications in functional, reversible, and quantum computing
    Thomas Knight, Jr. (MIT Artificial Intelligence Laboratory)
DP-COOL Session I - New Languages to support Multiparadigm Programming
  • SOUL and Smalltalk - Just Married
    Kris Gybels
  • Unifying Tables, Objects and Documents
    Erik Meijer and Wolfram Schulte
10.00 – 10.30: Coffee break
10.30 – 12.30
ICFP Session I
  • Scripting the type-inference process
    Bastiaan Heeren, Jurriaan Hage, and Doaitse Swierstra (Universiteit Utrecht)
  • Discriminative sum types locate the source of type errors
    Matthias Neubauer and Peter Thiemann (Universität Freiburg)
  • MLF: Raising ML to the power of system F
    Didier Le Botlan and Didier Rémy (INRIA Rocquencourt)
  • An extension of HM(X) with bounded existential and universal data-types
    Vincent Simonet (INRIA Rocquencourt)
LOPSTR Session I - Specification and Synthesis
  • Predicate synthesis from inductive proof attempt of faulty conjectures
    Moussa Demba, Khaled Bsaïes, and Francis Alexandre
  • Specification and Synthesis of Hybrid Automata for Physics-Based Animation
    Thomas Ellman
  • Adding Concrete Syntax to a Prolog-Based Program Synthesis System
    Bernd Fischer and Eelco Visser
  • Specifying Object-Oriented Systems in Computational Logic
    Kung-Kiu Lau and Mario Ornaghi
DP-COOL Session II - Multiparadigm Programming with C++ I
  • Syntax sugar for FC++: lambda, infix, monads and more
    Brian McNamara and Yannis Smaragdakis
  • Importing alternative programming paradigms into modern object-oriented languages
    Andrej Stolyarov
  • Program Templates: Expression Templates Applied to Program Evaluation
    Francis Maes
  • Discussion
12.30 – 14.15: Lunch
14.15 – 15.45
ICFP Session II
  • CDuce: an XML-centric general-purpose language
    Véronique Benzaken (LRI, Université Paris Sud, Orsay), Giuseppe Castagna (CNRS, LIENS, École Normale Supérieure), and Alain Frisch (LIENS, École Normale Supérieure, Paris)
  • Compiling regular patterns
    Michael Levin (University of Pennsylvania)
  • Software is discrete mathematics
    Rex Page (University of Oklahoma)
LOPSTR Session II - Verification
  • Building Satisfiability Procedures for Verification: The Case Study of Sorting Algorithms
    Abdessamad Imine and Silvio Ranise
  • Formal Development and Verification of Approximation Algorithms using Auxiliary Variables
    Rudolf Berghammer and Markus Müller-Olm
  • Formal Reasoning About Efficient Data Structures: A Case Study in ACL2
    José-Luis Ruiz-Reina, José-Antonio Alonso, María-José Hidalgo, and Francisco-Jesús Martín Mateos
DP-COOL Session III - Extending or using JAVA for Multiparadigm Programming
  • JSetL: Declarative Programming in JAVA with Sets
    Elisabetta Poleo and Gianfranco Rossi
  • SML2JAVA: a source to source translator
    Justin Koser, Haakon Larsen, Jeffrey Vaughan, and Dexter Kozen
  • Discussion
15.45 – 16:15: Tea break
16.15 – 18.00
ICFP Session III
  • Global abstraction-safe marshalling with hash types
    James Leifer, Gilles Peskine (INRIA Rocquencourt), Peter Sewell, and Keith Wansbrough (University of Cambridge)
  • Dynamic rebinding for marshalling and update, with destruct-time lambda
    Gavin Bierman (University of Cambridge), Michael Hicks (University of Maryland, College Park), Peter Sewell, Gareth Stoyle, and Keith Wansbrough (University of Cambridge)
  • Iterative-free program analysis
    Mizuhito Ogawa (Japan Advanced Institute of Science and Technology), Zhenjiang Hu (University of Tokyo) and Isao Sasano (Japan Advanced Institute of Technology and Science)
  • Report on ICFP 2003 & 2004
    Olin Shivers and Kathleen Fisher
LOPSTR Session III - Analysis
  • A Program Transformation for Backwards Analysis of Logic Programs
    John P. Gallagher
  • An Efficient Staging Algorithm for Binding-Time Analysis
    Takuma Murakami, Zhenjiang Hu, Kazuhiko Kakehi, and Masato Takeichi
  • Proving termination with adornments
    Alexander Serebrenik and Danny De Schreye
DP-COOL Session IV - Multiparadigm Programming with C++ II
  • Constraint Imperative Programming with C++
    Olaf Krzikalla
  • Patterns in Datatype-Generic Programming
    Jeremy Gibbons
  • A declarative approach to solve family polymorphism problem in C++
    Zoltan Prokolab and Istvan Zolyomi
  • Discussion / Summary
Tuesday 26/8
08:45 – 09:00
MERλIN Opening
09.00 – 10.00
ICFP invited talk
  • From Hilbert space to Dilbert space: Context semantics as a language for games and flow analysis
    Harry Mairson (Brandeis University)
MERλIN Invited talk
  • Scope, binding, and inlining in the Glasgow Haskell Compiler
    Simon Peyton-Jones (Microsoft Research, UK)
10.00 – 10.30: Coffee break
10.30 – 12.30
ICFP Session IV
  • A theory of aspects
    David Walker (Princeton University), Steve Zdancewic (University of Pennsylvania), and Jay Ligatti (Princeton University)
  • Dependency-style Generic Haskell
    Andres Löh, Dave Clarke, and Johan Jeuring (Universiteit Utrecht)
  • Functional automatic differentiation with Dirac impulses
    Henrik Nilsson (Yale University)
  • A user-centred approach to functions in Excel
    Simon Peyton Jones (Microsoft Research), Alan Blackwell (University of Cambridge), and Margaret Burnett (Oregon State University)
LOPSTR Session IV - Transformation
  • Constructively Characterizing Fold and Unfold
    Tjark Weber and James Caldwell
  • Deterministic Second-order Patterns in Program Transformation
    Tetsuo Yokoyama, Zhenjiang Hu, and Masato Takeichi
  • From Interpreter to Logic Engine: A Functional Derivation
    Dariusz Biernacki and Olivier Danvy
  • Linearization by Program Transformation
    Sandra Alves and Mário Florido
MERλIN Session I
  • Compiler Implementation in a Formal Logical Framework
    Jason Hickey, Aleksey Nogin, Adam Granicz, and Brian Aydemir
  • Verifying CPS transformations in Isabelle/HOL
    Yasuhiko Minamide and Koji Okuma
  • Mechanising Hankin and Barendregt using the Gordon-Melham axioms
    Michael Norrish
  • Reasoning on an Imperative Object-based Calculus in Higher Order Abstract Syntax
    Alberto Ciaffaglione, Luigi Liquori, and Marino Miculan
12.30 – 14.15: Lunch
14.15 – 15.45
ICFP Session V
  • A sound and complete axiomatization of delimited continuations
    Yukiyoshi Kameyama (University of Tsukuba) and Masahito Hasegawa (Kyoto University)
  • Call-by-value is dual to call-by-name
    Philip Wadler (Avaya Labs)
  • Disjunctive normal forms and local exceptions
    Emmanuel Beffara (Université Paris 7) and Vincent Danos (CRNS, Université Paris 7)
LOPSTR Session V - Specialisation
  • Invited Talk: Inductive Theorem Proving by Program Specialisation: Generating proofs for Isabelle using Ecce
    Michael Leuschel (work with Helko Lehmann)
  • Provable Correct Code Generation: A Case Study
    Qian Wang and Gopal Gupta
MERλIN Session III
  • A unified category-theoretic approach to variable binding
    John Power
  • A Definitional Approach to Primitive Recursion over Higher Order Abstract Syntax
    S. Ambler, R. Crole, and A. Momigliano
  • Representing Reductions of NP-Complete Problems in Logical Frameworks - A Case Study
    Jatin Shah and Carsten Schürmann
15.45 – 16:15: Tea break
16.15 – 18.00
ICFP Session VI
  • An effective theory of type refinements
    Yitzhak Mandelbaum, David Walker (Princeton University), and Robert Harper (Carnegie Mellon University)
  • A static type system for JVM access control
    Tomoyuki Higuchi and Atsushi Ohori (Japan Advanced Institute of Science and Technology)
  • Parsing polish, step by step (functional pearl)
    John Hughes (Chalmers University of Technology) and Doaitse Swierstra (Universiteit Utrecht)
  • Programming contest awards presentation
    John Hughes et al. (Chalmers University of Technology)
MERλIN Session IV
  • A Formalization of an Ordered Logical Framework in Hybrid with Applications to Continuation Machines
    Alberto Momigliano and Jeff Polakow
  • Towards a Dependent Modal Type Theory
    Aleksandar Nanevski, Brigitte Pientka, and Frank Pfenning
  • Explicit Substitutions and Higher Order Syntax
    Neil Ghani and Tarmo Uustalu
  • Swapping the Atom: Programming with Binders in Fresh O'Caml
    Mark R. Shinwell
  • Reasoning about Recursive Procedures with Parameters
    Ralph-Johan Back and Viorel Preoteasa
Wednesday 27/8
09.00 - 10.30
ICFP Session VII
  • Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism
    Geoffrey Washburn and Stephanie Weirich (University of Pennsylvania)
  • FreshML: Programming with binders made simple
    Mark Shinwell, Andrew Pitts, and Murdoch Gabbay (University of Cambridge)
  • Meta-programming through typeful code representation
    Chiyan Chen and Hongwei Xi (Boston University)
LOPSTR Session VI - Constraints
  • Simplification of database integrity constraints revisited: A transformational approach
    Henning Christiansen and Davide Martinenghi
  • Integration and Optimization of Rule-based Constraint Solvers
    Slim Abdennadher and Thom Frühwirth
  • Introducing ESRA, a Relational Language for Modelling Combinatorial Problems
    Pierre Flener, Justin Pearson, and Magnus Ågren
10.30 - 11.00: Coffee break
11.00 - 11.30
  • Optimistic evaluation: An adaptive evaluation strategy for non-strict programs
    Robert Ennals (University of Cambridge) and Simon Peyton Jones (Microsoft Research)
11.30 - 12.30
Joint ICFP & PPDP Invited talk
  • Understanding aspects
    Mitchell Wand (Northeastern University)
12.30 - 14.05: Lunch
14.05 - 14.15
PPDP Opening
14.15 - 15.45
PPDP Session I - Types, chaired by Benjamin Pierce
  • Rank 2 intersection types for modules
    Ferruccio Damiani (Universita' di Torino)
  • Generativity and Dynamic Opacity for Abstract Types
    Andreas Rossberg (Universität des Saarlandes)
  • From Dynamic Binding to State via Modal Possibility
    Aleksandar Nanevski (Carnegie Mellon University)
15.45 – 16:15: Tea break
16.15 - 17.45
PPDP Session II - Functional Language Implementation, chaired by Amr Sabry
  • A Functional Correspondence between Evaluators and Abstract Machines
    Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard (BRICS, University of Aarhus)
  • Compilation of extended recursion in call-by-value functional languages
    Tom Hirschowitz, Xavier Leroy (INRIA Rocquencourt), and Joe B. Wells (Heriot-Watt University)
  • Formally Deriving an STG Machine
    Alberto de la Encina and Ricardo Peña (Universidad Complutense de Madrid)
PLI Banquet
Thursday 28/8
08:45 – 09:00
Haskell Opening
09.00 - 10.30
PPDP Session II - Security, chaired by Dale Miller
  • Invited talk: Towards a Formal Notion of Trust
    Mogens Nielsen (BRICS, University of Aarhus)
  • Statically Assuring Secrecy for Dynamic Concurrent Processes
    Rachid Echahed, Frederic Prost (Laboratoire Leibniz), and Wendelin Serwe (INRIA)
Haskell Session I, chaired by Johan Jeuring
  • Functional pearl: Trouble shared is trouble halved
    Richard Bird and Ralf Hinze
  • The Yampa Arcade
    Antony Courtney, Henrik Nilsson, and John Peterson
  • XML Templates and Caching in WASH
    Peter Thiemann
10.30 - 11.00: Coffee break
11.00 - 12.30
PPDP Session III - Higher-Order Abstract Syntax, chaired by Alberto Momigliano
  • Explicit Substitutions in the Reduction of Lambda Terms
    Gopalan Nadathur and Xiaochu Qi (University of Minnesota)
  • A Framework for Typed HOAS and Semantics
    Marino Miculan and Ivan Scagnetto (DiMI, University of Udine)
  • Term Rewriting with Variable Binding: An Initial Algebra Approach
    Makoto Hamana (Gunma University)
Haskell Session II
  • Tool Support for Refactoring Functional Programs
    Huiqing Li, Claus Reinke, and Simon Thompson
  • Modeling Quantum Computing in Haskell
    Amr Sabry
  • Structure and Interpretation of Quantum Mechanics - a Functional Framework
    Jerzy Karczmarczuk
12.30 - 14.15: Lunch
14.15 - 15.45
PPDP Session IV - Evaluation of Logic Programs, chaired by Konstantinos Sagonas
  • Efficient Fixpoint Computation in Linear Tabling
    Neng-Fa Zhou (City University of New York) and Taisuke Sato (Tokyo Institute of Technology)
  • From Datalog Rules to Efficient Programs with Time and Space Guarantees
    Yanhong Liu and Scott Stoller (State University of New York at Stony Brook)
  • On the Rewriting and Efficient Computation of Bound Disjunctive Datalog
    Sergio Greco and Ester Zumpano (University of Calabria)
Haskell Session III, chaired by Olaf Chitil
  • Helium, for learning Haskell
    Bastiaan Heeren, Daan Leijen, and Arjan van IJzendoorn
  • Interactive Type Debugging in Haskell
    Peter J. Stuckey, Martin Sulzmann, and Jeremy Wazny
  • Tool Demo: HsDebug : Debugging Lazy Programs by not being Lazy
    Robert Ennals and Simon Peyton Jones
  • 10min Talk: A Pure Language with Default Strict Evaluation Order and Explicit Laziness
    Tim Sheard
15.45 – 16:15: Tea break
16.15 – 18.00
PPDP Session V - Constraints, chaired by Alessandra Di Pierro
  • Integrating Finite Domain Constraints and CLP with Sets
    Alessandro Dal Palu' (University of Udine), Agostino Dovier (University of Udine), Enrico Pontelli (New Mexico State University), and Gianfranco Rossi (University of Parma)
  • Extending constraint solvers with constraint handling rules
    Gregory Duck (University of Melbourne), Maria Garcia de la Banda (Monash University), Peter Stuckey (University of Melbourne), and Christian Holzbaur (University of Vienna)
  • Finding all minimal unsatisfiable subsets
    Maria Garcia de la Banda (Monash University), Peter Stuckey (University of Melbourne), and Jeremy Wazny (University of Melbourne)
Haskell Session IV, chaired by Magnus Carlsson
  • Haskell and Principal Types
    Karl-Filip Faxén
  • Simulating Quantified Class Constraints
    Valery Trifonov
  • Tool Demo: Haskell Tools from the Programatica Project
    Thomas Hallgren
  • 10min Talk: Records for Haskell
    Simon Peyton Jones
  • Discussion: The Future of Haskell
    Henrik Nilsson
Friday 29/8
08:30 - 09:00
Erlang Workshop Registration
09.00 - 10.30
PPDP Session VI - Verification, chaired by Frank Valencia
  • Invited talk: Automatic Verification of Cryptographic Protocols: A Logic Programming Approach
    Bruno Blanchet (Max Planck Institut für Informatik, Saarbrücken)
  • Foundational Proof Checkers with Small Witnesses
    Dinghao Wu, Andrew Appel (Princeton University), and Aaron Stump (Washington University in St. Louis)
Erlang Session I
  • Welcome / Introduction
  • Invited talk: Conceptual Integrity in Erlang or the Meaning of the !! Operator
    Joe Armstrong (SICS)
  • Evaluating Distributed Functional Languages for Telecommunications Software
    J.H. Nyström, P.W.Trinder (Heriot-Watt University), and D.J. King (Motorola)
10.30 - 11.00: Coffee break
11.00 - 12.30
PPDP Session VII - Debugging & Applications, chaired by Fergus Henderson
  • ViMer: a visual debugger for Mercury
    Michael Cameron, Maria Garcia de la Banda, Kim Marriott, and Peter Moulder (Monash University)
  • Practical aspects of Declarative Debugging in Haskell 98
    Bernard Pope and Lee Naish (The University of Melbourne)
  • On Translating Geometric Solids to Functional Expressions
    Omid Banyasad and Philip Cox (Dalhousie University)
Erlang Session II
  • Automated Test Generation for Industrial Erlang Applications
    Johan Blom and Bengt Jonsson (Uppsala University)
  • Extending the VoDKa Architecture to Improve Resource Modeling
    Juan José Sanchez Penas and Carlos Abalde Ramiro (University of A Coruña)
  • Armistice: An Experience Developing Management Software with Erlang
    David Cabrero, Carlos Abalde, Carlos Varela, and Laura Castro (University of A Coruña)
12.30 - 14.00: Lunch
14.00 - 16.00
PPDP Session VIII - Rewriting, chaired by Maria Alpuente
  • Termination of strategies in rule-based languages
    Olivier Fissore (LORIA-CNRS), Isabelle Gnaedig (LORIA-INRIA), and Helene Kirchner (LORIA-CNRS)
  • Conditional Narrowing without Conditions
    Sergio Antoy (Portland State University), Bernd Brassel, and Michael Hanus (CAU Kiel)
  • A Demand Narrowing Calculus with Overlapping Definitional Trees
    Rafael Del Vado (Universidad Complutense de Madrid)
  • Improving (Weakly) Outermost-Needed Narrowing: Natural Narrowing
    Santiago Escobar (DSIC-UPV)
14.00 - 15.30
Erlang Session III
  • Invited talk: Erlang Rationale
    Mike Williams (Ericsson)
  • Parametrized Modules in Erlang
    Richard Carlsson (Uppsala University)
  • All You Wanted to Know About the HIPE Compiler (and might have been afraid to ask)
    K. Sagonas, M. Pettersson, R. Carlsson, P. Gustafsson, and T. Lindahl (Uppsala University)
15.30 - 16:00: Tea break
16.00 - 17.30
Erlang Session IV
  • A Study of Erlang ETS Table Implementation and Performance
    Scott Lystig Fritchie (Snookles Music Consulting)
  • A Soft-typing System for Erlang
    Sven-Olof Nyström (Uppsala University)
  • Discussion / Report from the Program Committee / Closing comments