- Our apologies if you receive multiple copies of this message - ---------------------------------------------- | | | TLCA '99 | | | | Fourth International Conference on | | Typed Lambda Calculi and Applications | | | | April 7-9, 1999, L'Aquila (Italy) | | | ---------------------------------------------- PRELIMINARY SCHEDULE and CALL FOR PARTICIPATION ---------------------------------------------------------------------------- | Note the early registration and accommodation deadline: MARCH 7th, 1999. | ---------------------------------------------------------------------------- The Fourth International Conference on Typed Lambda Calculi and Applications (TLCA '99) will be held in L'Aquila (Italy) from 7th to 9th April, 1999. The conference is organized by the L'Aquila Computer Science Group at the Department of Pure and Applied Mathematics of the University of L'Aquila. You can find the preliminary schedule and all information about the conference venue, conference registration and hotel accommodation at the TLCA '99 web site: http://w3.dm.univaq.it/tlca99 For any further information, please contact the TLCA '99 Organizing Committee at the email address: tlca99.aquila@univaq.it ----------------------------------------------------------------------- PRELIMINARY SCHEDULE Wednesday, 7 April 1999 8.30 - 9.00 REGISTRATION Morning Session (Chairman: Jean-Yves Girard) 9.00 - 10.30 Tutorial: Denotational Semantics (Part I) Thomas Ehrhard 10.30 - 11.00 BREAK 11.00 - 11.30 Industrial Presentation: Application of Linear Logic to Distributed Object Coordination Jean-Marc Andreoli 11.30 - 12.00 Natural Deduction for Intuitionistic Non-Commutative Linear Logic Jeff Polakow and Frank Pfenning 12.00 - 12.30 Modules in non-commutative logic V. Michele Abrusci 12.30 - 14.30 LUNCH Afternoon Session (Chairman: Samson Abramsky) 14.30 - 16.00 Tutorial: Types: an Introduction Mariangiola Dezani 16.00 - 16.30 BREAK 16.30 - 17.00 Logical Predicates for Intuitionistic Linear Type Theories Masahito Hasegawa 17.00 - 17.30 Resource Interpretations, Bunched Implications and the alpha-lambda-calculus Peter O'Hearn 17.30 - 18.00 Elementary Complexity and Geometry of Interaction (Extended Abstract) Patrick Baillot and Marco Pedicini 18.00 - 18.30 A Study of Abramsky's Linear Chemical Abstract Machine Seikoh Mikami and Yohji Akama 18.30 - 19.00 Soundness of the Logical Framework for its Typed Operational Semantics Healfdene Goguen Thursday, 8 April 1999 Morning Session (Chairman: Thomas Streicher) 9.00 - 10.30 Tutorial: Denotational Semantics (Part II) </b></td> John Longley 10.30 - 11.00 BREAK 11.00 - 11.30 Strong Normalisation of Cut-Elimination in Classical Logic Christian Urban and Gavin Bierman 11.30 - 12.00 Explicitly typed lambda-mu-calculus for polymorphism and call-by-value Ken-etsu Fujita 12.00 - 12.30 Polarized Proof-Nets: Proof-Nets for LC (Extended Abstract) Olivier Laurent 12.30 - 14.30 LUNCH Afternoon Session (Chairman: Thierry Coquand) 14.30 - 15.00 Industrial Presentation: AnnoDomini in Practice: A Type-Theoretic Approach to the Year 2000 Problem Morten Heine Soerensen 15.00 - 15.30 Explicit Environments Masahiko Sato 15.30 - 16.00 Characterising Explicit Substitutions which Preserve Termination Eike Ritter 16.00 - 16.30 BREAK 16.30 - 17.00 Lambda Definability with Sums via Grothendieck Logical Relations Marcelo Fiore and Alex Simpson 17.00 - 17.30 Quantitative semantics revisited Nuno Barreiro and Thomas Ehrhard 17.30 - 18.00 Game semantics for untyped lambda-beta-eta-calculus Pietro Di Gianantonio, Gianluca Franco and Furio Honsell 18.00 - 18.30 Total Functionals and Well-founded Strategies Stefano Berardi and Ugo de' Liguoro 20.00 SOCIAL BANQUET with Banquet Speaker: Corrado Boehm. Friday, 9 April 1999 Morning Session (Chairman: Pawel Urzyczyn) 9.00 - 10.30 Tutorial: Intersection Types and Properties of Lambda-terms Mario Coppo 10.30 - 11.00 BREAK 11.00 - 11.30 Call-By-Push-Value: A Subsuming Paradigm Paul Blain Levy 11.30 - 12.00 Useless-code detection and elimination for PCF with algebraic Datatypes Ferruccio Damiani 12.00 - 12.30 A Curry-Howard isomorphism for compilation and program execution Atsushi Ohori 12.30 - 14.30 LUNCH Afternoon Session (Chairman: Simonetta Ronchi della Rocca) 14.30 - 15.00 Marginalia to a theorem of Jacopini Rick Statman 15.00 - 15.30 Every unsolvable lambda-term has a decoration Rene' David 15.30 - 16.00 Counting a type's principal inhabitants Sabine Broda and Luis Damas 16.00 - 16.30 BREAK 16.30 - 17.00 A Finite Axiomatization of Inductive-Recursive Definitions Anton Setzer and Peter Dybjer 17.00 - 17.30 A Logic for Abstract Data Types as Existential Types Erik Poll and Jan Zwanenburg 17.30 - 18.00 Pure Type Systems with Subtyping Jan Zwanenburg 18.00 END of TLCA'99 ----------------------------------------------------------- CONFERENCE INFORMATION Conference Venue ---------------- The TLCA '99 Conference will be held at the Centro Congressi of the Hotel Duca degli Abruzzi, Viale Giovanni XXIII, 10, in the centre of L'Aquila. The Centro Congressi is just nearby the Hotel Duca degli Abruzzi and at a walking distance from the other hotels with which special conference rates have been arranged (see below). Registration Fees ----------------- Before MARCH 7th After MARCH 7th Regular ITL 450.000 ITL 550.000 Full-time student ITL 350.000 ITL 450.000 The regular registration fee includes one copy of the Proceedings, coffee breaks, lunches and the social banquet. The student registration fee includes coffee breaks, lunches and the social banquet. Full-time students must certify their status. In order to pay the cheaper registration fee, you must register for the conference by returning the registration form below *via email* to the Organizing Committee at the email address: tlca99.aquila@univaq.it by MARCH 7th, 1999. Then, you can pay the registration fee either by cheque or bank transfer (with possible additional bank commissions) or by cash at the registration desk during the conference. Methods of Payment ------------------ Payment of the registration fee must be made in Italian Liras or Euros, net of all bank charges as follows: * Cheque or Bank Transfer on: account number: 70158/4 bank: CARISPAQ SpA, ABI code 6040 - CAB code 3601 address: Corso Vittorio Emanuele II, 48 67100 L'Aquila (Italy) * Cash at the conference desk A receipt of the registration will be issued by the TLCA'99 Organizing Committee. The TLCA'99 organizers cannot accept any liability for personal accidents, loss or damage of the private property of participants during the conference. The registration fee does not include any form of insurance. Conference participants are therefore responsible for making their own insurance arrangements. Please fill in the following registration form and return it via email to tlca99.aquila@univaq.it. ============================================================================ TLCA '99 - Registration Form ------------------------------ Family name ________________________________________________________ Name _____________________________ Middle Init. ________ Title _________ Affiliation __________________________________________________________ ___________________________________________________________________ Address ____________________________________________________________ ____________________________________________________________________ Postcode _______________________ City _________________________________ Country ________________________ State ________________________________ Phone _______________________________ Fax ____________________________ E-mail _______________________________ Dietary Restrictions (vegetarian, etc., please specify) _____________________________________________________________________ Accompanying person(s) ________________________________________________ Method of Payment of Registration Fee: [ ] Cheque [ ] Bank transfer [ ] Cash ============================================================================= Hotel Accommodation ------------------- We have arranged some conference rates with the hotels listed below. Reservations must be made as soon as possible in order to benefit from the conference rates. Such rates are guaranteed until MARCH 7th, 1999. Hotel DUCA DEGLI ABRUZZI *** Viale Giovanni XXIII, 10 67100 L'Aquila, Italy Phone: +39-0862-28341 Fax: +39-0862-61588 Hotel DUOMO *** Via Dragonetti, 10 67100 L'Aquila, Italy Phone: +39-0862-410893 Fax: +39-0862-413058 Hotel CASTELLO *** Piazza Battaglione Alpini (known as "Fontana Luminosa") 67100 L'Aquila, Italy Phone: +39-0862-419147 Fax: +39-0862-419140 All hotels are at a walking distance from the conference venue. Hotel Rates ----------- Room rates are given per room and per night, and include services, taxes, and continental breakfast. All prices are in Italian Liras. The (fixed) exchange rate with Euro is 1 Euro = 1936,27 ITL. Hotel Single room Double room Double x single Triple room Duca Degli Abruzzi ITL 90.000 ITL 126.000 ITL 117.000 ITL 156.000 Duomo ITL 95.000 ITL 145.000 ITL 120.000 ITL 160.000 Castello ---- ITL 145.000 ITL 120.000 ---- In order to book a room, you must fill in the following reservation form and *fax* it to the selected hotel by MARCH 7th, 1999. ============================================================================= TLCA '99 - Hotel Reservation Form ----------------------------------- Please tick the selected hotel: [ ] Hotel Duca degli Abruzzi [ ] Hotel Duomo [ ] Hotel Castello Please book me: N. ..... single room(s) N. ..... double room(s) N. ..... triple room(s) Date of arrival ................................ Date of departure .............................. N. of nights .......... Credit Card number ............................................... Expiry date ............................... [ ] Visa [ ] Eurocard/Mastercard [ ] American Express Holder's name .......................................................... (The credit card number is only taken as guarantee without being charged). ============================================================================= How to Reach L'Aquila --------------------- L'Aquila is about 100 Km East of Rome. The nearest airport is Rome Fiumicino (FCO). L'Aquila can be easily reached by bus or car. Train service is also available, though less advisable, since it takes a longer time due to intermediate train stops. By bus: L'Aquila can be reached by taking the ARPA bus from the train station Roma Tiburtina. The train service from the Fiumicino Airport to Roma Tiburtina is available from 6.55 am to 10 pm every 20 minutes (travelling time: 40 min; a train ticket costs ITL 7.000). If you reach Rome by means of a train that does not stop at Roma Tiburtina, you can get off at Roma Termini or Roma Ostiense, then take the metro (line B, direction Rebibbia) and stop at Tiburtina FS. The time schedule of the ARPA bus from Roma Tiburtina to L'Aquila is as follows: Weekdays 6.15 - 6.45 - 7.30 - 8.10 - 10.00 - 11.00 - 12.25 - 13.20 - 14.15 - 14.45 - 15.15 - 16.15 - 17.15 - 17.45 - 18.45 - 19.30 - 21.00 - 22.45 Holidays 8.10 - 11.00 - 13.30 - 15.00 - 18.00 - 19.00 - 19.30 - 21.00 - 22.00 - 22.15 - 22.45 A bus ticket costs ITL 16.900 and must be bought before boarding the bus, at the ARPA agency. The trip lasts about 1 hour and 40 minutes. The bus terminal in L'Aquila is at Fontana Luminosa near the Castello Cinquecentesco. The time schedule of the ARPA bus from L'Aquila (Fontana Luminosa) to Roma Tiburtina is as follows: Weekdays 4.40 - 5.40 - 6.45 - 8.00 - 9.00 - 10.10 - 11.00 - 13.00 - 13.30 - 14.05 - 15.10 - 15.20 - 17.15 - 18.00 - 19.00 - 20.00 Holidays 6.00 - 8.00 - 10.10 - 12.30 - 15.00 - 15.20 - 18.00 - 19.00 - 20.00 L'Aquila can also be reached by bus from Pescara. The time schedule is as follows: Weekdays 6.00 - 6.35* - 8.00 - 8.30* - 10.30* - 13.10 - 14.05 - 17.50 - 19.30 Holidays 8.00 - 13.00 - 18.00 - 19.45 *Via road (the others via motorway) The trip lasts 1 hour and 50 minutes via motorway, and 2 hours and 20 minutes via road. The bus terminal in L'Aquila is at Fontana Luminosa near the Castello Cinquecentesco. By car: L'Aquila can be reached via motorway or road:
From Rome : Motorway A24 Roma-L'Aquila or by Via Salaria Roma-Rieti-L'Aquila
From Autostrada Adriatica (Motorway A14): Casello Roseto - Traforo del Gran Sasso - L'Aquila
From Pescara: Motorway A25 Pescara-Popoli and then S.S 17 Bussi-L'Aquila
From Napoli: Motorway A2 Roma-Napoli - S.S. 82 Ceprano-Sora-Avezzano - Motorway Avezzano-L'Aquila A24/A25
---------------------------------------------------------------------------- %%%%%%%%%%%%%%% LATEX VERSION OF PRELIMINARY SCHEDULE %%%%%%%%%%%%%% \documentclass[11pt]{article} \topmargin -0.5 cm \oddsidemargin 0cm \evensidemargin 0cm \textwidth 16cm \textheight 24cm \parindent 0.5cm \renewcommand{\thepage}{\mbox{}} \newcommand{\Item}[3]{{\bf #1} & {\em #2} \\ & #3 \\ [3mm] } \newcommand{\Jtem}[2]{{\bf #1} & #2 \\ [3mm] } \newcommand{\Invtem}[4]{{\bf #1} & #2 \\ & {\em #3} \\ & #4 \\ [3mm] } \begin{document} \begin{center} \Large \bf{Typed Lambda Calculi and Applications (TLCA '99) \\ [5mm] April 7-9, 1999 \\ [5mm] L'Aquila (Italy) \\ [30mm] Preliminary Schedule} \end{center} \newpage \begin{center}\Large \bf{Wednesday, 7 April 1999} \end{center} \vspace{10mm} \hspace{7mm} {\bf {8.30 - 9.00}} \hspace{3mm} REGISTRATION \vspace{3mm} \noindent \large{Morning Session (Chairman: Jean-Yves Girard)} \vspace{3mm} \begin{tabular}{rl} \Invtem{9.00 - 10.30}{Tutorial:}{Denotational Semantics (Part I)} {Thomas Ehrhard} \Jtem{10.30 - 11.00}{BREAK} \Invtem{11.00 - 11.30}{Industrial Presentation:}{Application of Linear Logic to Distributed Object Coordination} {Jean-Marc Andreoli} \Item{11.30 - 12.00}{Natural Deduction for Intuitionistic Non-Commutative Linear Logic} {Jeff Polakow and Frank Pfenning} \Item{12.00 - 12.30}{Modules in non-commutative logic} {V. Michele Abrusci} \Jtem{12.30 - 14.30}{LUNCH} \end{tabular} \vspace{3mm} \noindent \large{Afternoon Session (Chairman: Samson Abramsky)} \vspace{3mm} \begin{tabular}{rl} \Invtem{14.30 - 16.00}{Tutorial:}{Types: an Introduction} {Mariangiola Dezani} \Jtem{16.00 - 16.30}{BREAK} \Item{16.30 - 17.00}{Logical Predicates for Intuitionistic Linear Type Theories} {Masahito Hasegawa} \Item{17.00 - 17.30}{Resource Interpretations, Bunched Implications and the $\alpha \lambda$-calculus} {Peter O'Hearn} \Item{17.30 - 18.00}{Elementary Complexity and Geometry of Interaction (Extended Abstract)} {Patrick Baillot and Marco Pedicini} \Item{18.00 - 18.30}{A Study of Abramsky's Linear Chemical Abstract Machine} {Seikoh Mikami and Yohji Akama} \Item{18.30 - 19.00}{Soundness of the Logical Framework for its Typed Operational Semantics} {Healfdene Goguen} \end{tabular} \newpage \begin{center}{\Large \bf{Thursday, 8 April 1999}} \end{center} \vspace{10mm} \noindent \large{Morning Session (Chairman: Thomas Streicher)} \vspace{3mm} \begin{tabular}{rl} \Invtem{9.00 - 10.30}{Tutorial}{Denotational Semantics (Part II)} {John Longley} \Jtem{10.30 - 11.00}{BREAK} \Item{11.00 - 11.30}{Strong Normalisation of Cut-Elimination in Classical Logic} {Christian Urban and Gavin Bierman} \Item{11.30 - 12.00}{Explicitly typed $\lambda \mu$-calculus for polymorphism and call-by-value} {Ken-etsu Fujita} \Item{12.00 - 12.30}{Polarized Proof-Nets: Proof-Nets for LC (Extended Abstract)} {Olivier Laurent} \Jtem{12.30 - 14.30}{LUNCH} \end{tabular} \vspace{3mm} \noindent \large{Afternoon Session (Chairman: Thierry Coquand)} \vspace{3mm} \begin{tabular}{rl} \Invtem{14.30 - 15.00}{Industrial Presentation: {\em AnnoDomini in Practice:}} {A Type-Theoretic Approach to the Year 2000 Problem} {Morten Heine S{\o}rensen} \Item{15.00 - 15.30}{Explicit Environments} {Masahiko Sato} \Item{15.30 - 16.00}{Characterising Explicit Substitutions which Preserve Termination} {Eike Ritter} \Jtem{16.00 - 16.30}{BREAK} \Item{16.30 - 17.00}{Lambda Definability with Sums via Grothendieck Logical Relations} {Marcelo Fiore and Alex Simpson} \Item{17.00 - 17.30}{Quantitative semantics revisited} {Nuno Barreiro and Thomas Ehrhard} \Item{17.30 - 18.00}{Game semantics for untyped $\lambda \beta \eta$-calculus} {Pietro Di Gianantonio, Gianluca Franco and Furio Honsell} \Item{18.00 - 18.30}{Total Functionals and Well-founded Strategies} {Stefano Berardi and Ugo de' Liguoro} \Jtem{20.00}{SOCIAL BANQUET with Banquet Speaker: Corrado B\"{o}hm.} \end{tabular} \newpage \begin{center}{\Large \bf{Friday, 9 April 1999}} \end{center} \vspace{10mm} \noindent \large{Morning Session (Chairman: Pawel Urzyczyn)} \vspace{3mm} \begin{tabular}{rl} \Invtem{9.00 - 10.30}{Tutorial:}{Intersection Types and Properties of $\lambda$-terms} {Mario Coppo} \Jtem{10.30 - 11.00}{BREAK} \Item{11.00 - 11.30}{Call-By-Push-Value: A Subsuming Paradigm} {Paul Blain Levy} \Item{11.30 - 12.00}{Useless-code detection and elimination for PCF with algebraic Datatypes} {Ferruccio Damiani} \Item{12.00 - 12.30}{A Curry-Howard isomorphism for compilation and program execution} {Atsushi Ohori} \Jtem{12.30 - 14.30}{LUNCH} \end{tabular} \vspace{3mm} \noindent \large{Afternoon Session (Chairman: Simonetta Ronchi della Rocca)} \vspace{3mm} \begin{tabular}{rl} \Item{14.30 - 15.00}{Marginalia to a theorem of Jacopini} {Rick Statman} \Item{15.00 - 15.30}{Every unsolvable $\lambda$-term has a decoration} {Ren\'e David} \Item{15.30 - 16.00}{Counting a type's principal inhabitants} {Sabine Broda and Luis Damas} \Jtem{16.00 - 16.30}{BREAK} \Item{16.30 - 17.00}{A Finite Axiomatization of Inductive-Recursive Definitions} {Anton Setzer and Peter Dybjer} \Item{17.00 - 17.30}{A Logic for Abstract Data Types as Existential Types} {Erik Poll and Jan Zwanenburg} \Item{17.30 - 18.00}{Pure Type Systems with Subtyping} {Jan Zwanenburg} \Jtem{18.00}{END of TLCA'99} \end{tabular} \end{document} ----------------------------------------------------------- Organizing Committee Chairman: Benedetto Intrigila Dipartimento di Matematica Pura ed Applicata Universita' degli Studi di L'Aquila via Vetoio, Loc. Coppito 67100 L'Aquila Italy fax: (+)-39-0862-433180 e-mail: tlca99.aquila@univaq.it home page: http://w3.dm.univaq.it/tlca99 -----------------------------------------------------------