[Prev][Next][Index][Thread]

TLCA '95: Programme


\documentstyle{article}
\begin{document}
\newcommand{\Paper}[2] {{\it #1},$\;${#2}}

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

\author{}\date{}
\maketitle

\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
terminate}
{P.A.~Mellies}\\
9.30 \Paper{Comparing $\lambda$-calculus translations in sharing graphs}
{A.~Asperti, C.~Laneve}\\
10.00           Coffee\\

10.30
\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} \\
\end{tabbing}


\newpage
\begin{tabbing}
\\
{\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}
{G.~Barthe}\\

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
Choice},\\
      \> {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\\
\end{tabbing}


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

9.00
\Paper{A verified typechecker}
{R.~Pollack}\\

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


10.00           Coffee\\

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

11.00
\Paper{A simple model for quotient types}
{M.~Hofmann}\\

11.30
\Paper{$\lambda$-calculus, combinators and comprehension systems}
{G.~Dowek}\\

\\
12.00           Lunch\\
\\

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

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

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


3.00            Tea\\

{\bf Decision Problems}\\

3.30
\Paper{Third-order matching in the presence of type constructors}
{J.~Springintveld}\\

4.00
\Paper{On equivalence classes of interpolation equations}
{V.~Padovani}\\


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

\end{document}