Preface Volume 37

AbstractThis volume contains the Proceedings of the Workshop on Type-Theoretic Languages: Proof Search and Semantics. The Workshop was held in CMU, Pittsburgh on June 20 and 21, 2000, in conjunction with CADE-17 Conference.Much recent work has been devoted to type theory and its applications to proof-and program-development in various logical settings. The focus of this workshop is on proof-search, with a specific interest on semantic aspects of, and semantics approaches to, type-theoretic languages and their underlying logics (e.g., classical, intuitionistic, linear, substructural). Such languages can be seen as logical frameworks for representing proofs and in some cases formalize connections between proofs and programs that support program-synthesis.The theory of proof-search has developed mostly along proof-theoretic lines but using many type-theoretic techniques. The utility of type-theoretic methods suggests that semantic methods of the kind found to be valuable in the semantics of programming languages should be useful in tackling the main outstanding difficulty in the theory of proof-search, i.e., the representation of intermediate stages in the search for a proof.The objective of the workshop is to provide a forum for discussion between, on the one hand, researchers interested in all aspects of proof-search in type theory, logical frameworks and their underlying (e.g., classical, intuitionistic, substructural) logics and, on the other, researchers interested in the semantics of computation. Topics of interest, in this context, include but are not restricted to the following: Foundations of proof-search in type-theoretic languages (sequent calculi, natural deduction, logical frameworks, etc.); Systems, methods and techniques related to proof construction or to counter-models generation (tableaux, matrix, resolution, semantic techniques, proof plans, etc.); Decision procedures, strategies, complexity results; Logic programming as search-based computation, integration of model-theoretic semantics, semantics foundations for search spaces; Computational models based on structures as games and realizability; Proof synthesis vs program synthesis and applications, equational theories and rewriting; Applications of proof-theoretic and semantics techniques to the design and implementation of theorem provers.Many thanks to the Program Committee, consisting of Didier Galmiche (LORIA – Universite Henri Poincare, Nancy, France), Patrick Lincoln (SRI, Stanford, U.S.A.), Frank Pfenning (Carnegie Mellon University, Pittsburgh, U.S.A.), David Pym (Queen Mary and Westfield College, London, U.K.), Jan Smith (Chalmers University, G/{o}teborg, Sweden.), for their scientific work during the preparation of the workshop. Many thanks to the participants and also to Frank Pfenning who has kindly accepted to replace an invited lecturer not in position to participate, by giving a talk on his work with R. Davies about (A Judgemental Reconstruction of Modal Logic).We would like also to take this opportunity to thank Michael Mislove for his invitation to publish the proceedings in the ENTCS series.This volume will be published as volume 37 in the series Electronic Notes in Theoretical Computer Science (ENTCS). This series is published electronically through the facilities of Elsevier Science B.V. and its auspices. The volumes in the ENTCS series can be accessed at the URLhttp://www.elsevier.nl/locate/entcsOctober 15, 2000Didier Galmich