Abstract
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 be- tween proofs and programs that support program-synthesis.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Galmiche, D. (2000). Workshop: Type-Theoretic Languages: Proof-Search and Semantics. In: McAllester, D. (eds) Automated Deduction - CADE-17. CADE 2000. Lecture Notes in Computer Science(), vol 1831. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10721959_47
Download citation
DOI: https://doi.org/10.1007/10721959_47
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67664-5
Online ISBN: 978-3-540-45101-3
eBook Packages: Springer Book Archive