 |
PLI'03 Program: Day by day
Sunday 24/8
19.00
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
ICFP Session VIII
- 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)
19.30
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
|