The First International Workshop on Explicit Substitutions:

Theory and Applications to Programs and Proofs

March 29, 1998, Tsukuba, Japan

This workshop is organized in conjunction with RTA-98

WESTAPP 98

	ULTRA group Useful Logics, Types, Rewriting, and Applications		UKII UK Institute of Informatics, UK
	The Engineering and Physical Sciences Research Council (EPSRC)

 9:00 - 10:00  invited talk I


Pierre-Louis Curien (Ecole Normale Supérieure+CNRS Paris)

10:00 - 10:30  coffee break


10:30 - 12:00  session I

Two Calculi of Explicit Substitution with Confluence
  on Metaterms and Preservation of Strong Normalisation (1st order and with
  names) and their equivalence
Kristoffer Høgsbro Rose and 
Frédéric Lang,  (Lyon)
An Explicit Substitution Notation in a Lambda Prolog Implementation
Gopalan Nadathur (Chicago)


12:00 - 13:15  lunch break


13:15 - 14:15  invited talk II

Therese Hardin (Université Paris 6)



14:15 - 15:00  session II

An Explicit Natural Deduction
Bruno Pagano (Paris)


15:00 - 15:30  tea break


15:30 - 17:45  session III

Proof Synthesis via Refinement Steps: Another Application of Explicit Substitutions on Open Terms
César Muñoz (Menlo Park)
Linear Explicit Substitutions
Neil Ghani, 
Valeria de Paiva and 
Eike Ritter (Birmingham)
Translations of First-Class Environments to Records
Shin-ya Nishizaki (Chiba), 
Yohji Akama (Tokyo)


18:00 -  RTA98 reception