Preface

TL;DRAbstract

This 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 pro

Chat with Paper

AI Agents for this Paper