2-5 Mar 2020
Torino, Italy
============================== --------------------------------------------------------------------- Call For Participation to TYPES 2020 --------------------------------------------------------------------- ================================================== 26th INTERNATIONAL CONFERENCE ON TYPES FOR PROOFS AND PROGRAMS 2020 ================================================== https://types2020.di.unito.it Turin, Italy, TYPES 2-5 March and ITRS 6 March 2020 The TYPES meetings are a forum to present new and on-going work in all aspects of type theory and its applications, especially in formalised and computer assisted reasoning and computer programming. The TYPES areas of interest include, but are not limited to: * foundations of type theory and constructive mathematics; * applications of type theory; * dependently typed programming; * industrial uses of type theory technology; * meta-theoretic studies of type systems; * proof assistants and proof technology; * automation in computer-assisted reasoning; * links between type theory and functional programming; * formalizing mathematics using type theory. We host talks proposing new ways of applying type theory. In the spirit of workshops, talks may be based on newly published papers, work submitted for publication, but also work in progress. The EUTypes Cost Action CA15123 (eutypes.cs.ru.nl) focuses on the same research topics as TYPES and partially sponsors the TYPES Conference: Part of the program is organised under the auspices of EUTypes. INVITED SPEAKERS * Ulrik Buchholtz * Pierre Marie-Pdrot * Leonardo de Moura * Sara Negri The ITRS 2020 workshop aims to bring together researchers working on both the theory and practical applications of systems based on intersection types and related approaches. Topics include, but are not limited to: Formal properties of systems with intersection types. Results for related systems, such as union types, refinement types, or singleton types. Applications to lambda calculus, pi-calculus and similar systems. Applications for programming languages, program analysis, and program verification. Applications for other areas, such as database query languages and program extraction from proofs. Related approaches using behavioural/intensional types and/or denotational semantics to characterize computational properties. Quantitative refinements of intersection types. Invited Speaker - Jeremy Siek (Indiana University Bloomington) Registration form: https://types2020.di.unito.it/registration.html Early registration: 12th February CONTACT Ugo de'Liguoro Email: ugo.deliguoro@unito.it -- [LOGIC] mailing list http://www.dvmlg.de/mailingliste.html Archive: http://www.illc.uva.nl/LogicList/ provided by a collaboration of the DVMLG, the Maths Departments in Bonn and Hamburg, and the ILLC at the Universiteit van Amsterdam