TLCA '95: Programme

\newcommand{\Paper}[2] {{\it #1},$\;${#2}}

   International Conference on \\
Typed Lambda Calculi and Applications\\
{\normalsize Edinburgh, April 10th - 12th, 1995}}


\begin{tabbing} {\bf MONDAY}\\

Morning Session Chaired by: M.~Dezani\\
{\bf Theory of Reduction and Conversion}\\
9.00 \Paper{Typed $\lambda$-calculi with explicit substitutions may not
9.30 \Paper{Comparing $\lambda$-calculus translations in sharing graphs}
{A.~Asperti, C.~Laneve}\\
10.00           Coffee\\

\Paper{Typed operational semantics}{H.~Goguen}\\

11.00 \Paper{An explicit eta rewrite rule} {D. Briaud}\\

11.30 \Paper{$\beta\eta$-equality for coproducts} {N.~Ghani} \\
12.00           Lunch \\
Afternoon Session Chaired by: G.~Plotkin\\
{\bf Semantics I}\\
2.00   \= {\it A fully abstract translation between a $\lambda$-calculus
with reference types and }\\
       \>  {\it standard ML,} {E.~Ritter, A.M.~Pitts}\\

2.30 \Paper{Final semantics for untyped $\lambda$-calculus} {F.~Honsell,
M.~Lenisa} \\
3.00            Tea \\
{\bf Categorical Semantics}\\
3.30 \Paper{What is a categorical model of intuitionistic linear logic?}
{G.M.~Bierman} \\
4.00  \= {\it Categorical semantics of the call-by-value $\lambda$-calculus,}\\
      \> {A.~Pravato, S.~Ronchi della Rocca, L.~Roversi}\\

4.30 \Paper{Categorical completeness results for the simply-typed
$\lambda$-calculus} {A.K.~Simpson} \\

{\bf TUESDAY}\\
Morning Session Chaired by: H.~Barendregt\\
{\bf Type Theory I}\\
9.00 \Paper{Untyped $\lambda$-calculus with relative typing} {M.R.~Holmes}\\

9.30 \Paper{Basic properties of data types with inequational refinements}
{H.~Kondoh} \\

10.00           Coffee\\

10.30 \Paper{Extensions of pure type systems}

11.00 \Paper{A simple calculus of exception handling} {P.~de Groote}\\

{\bf Proof Theory}\\
11.30 \Paper{Strict functionals for termination proofs}
{J.~van de Pol, H.~Schwichtenberg} \\

12.00           Lunch\\

Afternoon Session Chaired by: F.~Honsell\\
{\bf Semantics II}\\
2.00 \Paper{A simplification of Girard's paradox} {A.J.~Hurkens}\\

2.30  \= {\it A realization of the negative interpretation of the Axiom of
      \> {S.~Berardi, M.~Bezem, T.~Coquand}\\

3.00            Tea\\

3.30  \=  {\it A model for formal parametric polymorphism: a per
interpretation of}\\
      \>  {\it system $\cal R$}, {R.~Bellucci, M.~Abadi, P.L.~Curien}\\

4.00 \Paper{Expanding extensional polymorphism} {R.~Di Cosmo, A.~Piperno}\\

{\bf Discussion}\\
4.30 Open Problem Session, H. Barendregt\\

Morning Session Chaired by: J.~Smith\\
{\bf Machine Assisted Reasoning I}\\

\Paper{A verified typechecker}

\Paper{Higher-order abstract syntax in Coq}
{J.~Despeyroux, A.~Felty, A.~Hirschowitz}\\

10.00           Coffee\\

{\bf Type Theory II}\\
\Paper{Using subtyping in program optimization}
{S.~Berardi, L.~Boerio}\\

\Paper{A simple model for quotient types}

\Paper{$\lambda$-calculus, combinators and comprehension systems}

12.00           Lunch\\

Afternoon Session Chaired by: R.~Hindley\\
{\bf Machine Assisted Reasoning II}\\

\Paper{Extracting text from proof}
{Y.~Coscoy, G.~Kahn, L.~Thery}\\

 \= {\it Termination proof of term rewriting system with the multiset path
ordering and}\\
 \> {\it  derivation length. A complete development in the Calculus of
 \> {F.~Leclerc}\\

3.00            Tea\\

{\bf Decision Problems}\\

\Paper{Third-order matching in the presence of type constructors}

\Paper{On equivalence classes of interpolation equations}

\Paper{Decidable properties of intersection type systems}
{T.~Kurata, M.~Takahashi}\\