[TYPES/announce] Second DeepSpec Summer School, July 16-27, 2018
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Applications are now invited for participation in the Second DeepSpec Summer School (DSSS'18) Princeton, NJ, July 16-27, 2018 https://deepspec.org/event/dsss18 Overview Can critical systems be built according to functionally precise specifications of of their constituent components (processor, operating system, crypto library,..) and development tools (compilers, synthesis tools)? This may seem a pipe dream, but the past decade has seen remarkable advances in the technology required to realize it. The DeepSpec summer school will provide students with knowledge and experience necessary for understanding the state of the art and for contributing to ongoing research efforts, based on the interactive proof assistant Coq. The school is supported by generous funding from the National Science Foundation. DSSS'18 will consist of two parts with the first week being devoted to introductory topics and the second week covering current research efforts. July 16-18 (Mon-Wed)Coq Intensive July 19-20 (Thu-Fri)Fundamental proof techniques and project overviews July 23-27 (week 2) Advanced topics in system verification Lecturers and Topics for week 2 --- Andrew Appel andVerifiable C: a logic and toolset for Lennart Beringerproving C programs correct Adam Chlipala Implementing, specifying, verifying, and compiling hardware components with Kami Zach TatlockVerifying distributed systems Benjamin Pierce Property-based random testing with QuickChick All DeepSpec PIsTowards the specification and verification of a web server Prerequisites - DSSS'18 is aimed at a wide range of participants, including graduate students, academics, and industrial engineers and researchers. The Coq proof assistant will serve as a lingua franca for all the lectures. Participants who are not familiar with Coq at the level of Software Foundations (Volume 1) should plan on attending the Coq Intensive. Participants unfamiliar with volumes 2 and 3 may benefit from attending the last 3 days of week 1. Participants of DSSS'17 are likely to be admitted for participation in week 2 only. Application and participation - Participation in DSSS'18 is by invitation only, based on an application process that is open to anybody. To apply, please fill this application form https://www.regonline.com/builder/site/?eventid=2209458 preferably no later than March 23, 2018. Accepted participants will be notified shortly thereafter, and will be invited to confirm their participation by registering. Thanks to the generosity of NSF, we will be able to provide substantial financial assistance to all participants. We will not charge a registration fee, and will offer free dorm accommodation on the campus of Princeton University. In addition, we expect to subsidize travel expenses for the majority of participants, based on their geographic origin, qualification, and financial needs. To help us allocating these funds, the application form includes the option to enter estimated travel costs etc.. Late applications will be handled on a case-by-case basis. For additional information on the DeepSpec project, please see https://deepspec.org.
[TYPES/announce] ThEdu'18: Call for Extended Abstracts & Demonstrations
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] (Apologies for duplicates) Call for Extended Abstracts & Demonstrations ** ThEdu'18 Theorem proving components for Educational software 18 July 2018 http://www.uc.pt/en/congressos/thedu/thedu18 ** at FLoC 2018 Federated Logic Conference 2018 6-19 July 2018 Oxford, UK http://www.floc2018.org/ ** THedu'18 Scope: Computer Theorem Proving is becoming a paradigm as well as a technological base for a new generation of educational software in science, technology, engineering and mathematics. The workshop brings together experts in automated deduction with experts in education in order to further clarify the shape of the new software generation and to discuss existing systems. Invited Talk Julien Narboux, University of Strasbourg, France Important Dates * Extended Abstracts: 15th April 2018 * Author Notification: 15th May 2018 * Workshop Day:18 July 2018 Topics of interest include: * methods of automated deduction applied to checking students' input; * methods of automated deduction applied to prove post-conditions for particular problem solutions; * combinations of deduction and computation enabling systems to propose next steps; * automated provers specific for dynamic geometry systems; * proof and proving in mathematics education. Submission We welcome submission of extended abstracts and demonstration proposals presenting original unpublished work which is not been submitted for publication elsewhere. All accepted extended abstracts and demonstrations will be presented at the workshop. The extended abstracts will be made available online. Extended abstracts and demonstration proposals should be submitted via easychair, https://easychair.org/conferences/?conf=thedu18 formatted according to http://www.easychair.org/publications/easychair.zip Extended abstracts and demonstration proposals should be approximately 5 pages in length and are to be submitted in PDF format. At least one author of each accepted extended abstract/demonstration proposal is expected to attend THedu'18 and presents his/her extended abstract/demonstration. Program Committee Francisco Botana, University of Vigo at Pontevedra, Spain Roman Hašek, University of South Bohemia, Czech Republic Filip Maric, University of Belgrade, Serbia Walther Neuper, Graz University of Technology, Austria (co-chair) Pavel Pech, University of South Bohemia, Czech Republic Pedro Quaresma, University of Coimbra, Portugal (co-chair) Vanda Santos, CISUC, Portugal Wolfgang Schreiner, Johannes Kepler University, Austria Burkhart Wolff, University Paris-Sud, France Proceedings The extended abstracts and system descriptions will be available in ThEdu'18 Web-page. After presentation at the conference, selected authors will be invited to submit a substantially revised version, extended to 14--20 pages, for publication by the Electronic Proceedings in Theoretical Computer Science (EPTCS). -- Dr. Achim D. Brucker | Software Assurance & Security | University of Sheffield https://www.brucker.ch | https://logicalhacking.com/blog @adbrucker | @logicalhacking
[TYPES/announce] Fully funded PhD scholarship at the IT University of Copenhagen
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dear all, As part of the research project Type Theories for Reactive Programming funded by Villum Fonden, I have an opening for a fully funded PhD scholarship at the IT University of Copenhagen starting this year. The aim of the project is to construct a (dependent) type theory for programming and reasoning about reactive systems, using modalities to encode productivity. The design of the type theory will be based on denotational models, so the ideal candidate will have knowledge of category theory and type theory, but this is not a requirement. Further details on the project and how to apply can be found here: https://tinyurl.com/y87wnwnq Please feel free also to contact me directly for further details. A more detailed description of the project can be found below. Best wishes, Rasmus Møgelberg - Project description Type theories are formal systems that can be viewed both as programming languages and logical systems for formalised mathematics. From a computer science perspective this is useful because it allows for programs, their specifications, and the proofs that these satisfy the specification to be expressed in the same formalism. The logical interpretation of type theories means that all programs must terminate. For this reason, programming and reasoning about non-terminating reactive programs in type theory remains a challenge. This is unfortunate since these include many of the most critical programs in use today. In this project we aim to design a new type theory useful for programming with and reasoning about reactive programs. We build on recent progress in guarded recursion and functional reactive programming, using modal type constructors to capture productivity in types, as well as other recent advances in type theory, including homotopy type theory. We will use mathematical modelling when constructing the type theory and reasoning about consistency. The preferred candidate will therefore have knowledge of category theory and denotational semantics, but this is not a requirement. Experience with type theory or proof assistants is also an advantage, but not required.
