\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}