Subject: categories: TLCA'99 Call for Participation (Text & LaTex versions)

From: "tlca99.aquila" <[email-masked]>
Date: Fri, 5 Feb 1999 11:06:20 +0100 (MET)

- 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: 

                  [email-masked]  

----------------------------------------------------------------------- 
                  
                    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: 

                 [email-masked] 

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 [email-masked]. 

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

                     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: [email-masked]
home page: http://w3.dm.univaq.it/tlca99
-----------------------------------------------------------