[TYPES/announce] Third DeepSpec Summer School, July 13-24, 2020
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Applications are now invited for participation in the Third DeepSpec Summer School (DSSS'20) New Haven, CT, July 13-24, 2020 https://deepspec.org/event/dsss20 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'20 will consist of two parts with the first week being devoted to introductory topics and the second week covering current research efforts. July 13-15 (Mon-Wed)Coq intensive; CertiKOS design & spec July 16-17 (Thu-Fri)Fundamental proof techniques and project overviews July 20-24 (week 2) Advanced topics in system verification - Week 1 begins with a Coq Intensive, introducing our favorite proof assistant (used in almost all other lectures), with no assumption of formal-methods experience. A mix of lecturers (who will also present research lectures later in the program) will cover this material. - For participants who already know the Coq Intensive material, we will offer a Week 1 parallel track taught by Zhong Shao, on the CertiKOS operating-system framework, focused on the compositional specification and implementation of C modules, setting up to learn how to prove these modules in Week 2. - Week 1 ends with lectures by Andrew Appel, on verified functional algorithms; and Joe Tassarotti, on theory and computer-systems applications of the Iris verification framework for concurrency. - Week 2 includes lectures by Adam Chlipala, on connecting proofs of hardware and software components for embedded systems; Benjamin Pierce, on random testing and an application to web servers; Zhong Shao, on operating-system verification; Matthieu Sozeau, on the MetaCoq framework and (as a representative of the Coq team at Inria) recent improvements in and latest roadmap for Coq; Stephanie Weirich, on verifying functional algorithms written in Haskell; and Steve Zdancewic, on the Interaction Trees formalism and its applications to compilers and testing. - There will be ample opportunity for self-study/homework, student presentations, and other activities. Prerequisites - DSSS'20 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 and DSSS'18 are likely to be admitted for participation in week 2 only. Application and participation - Participation in DSSS'20 is by invitation only, based on an application process that is open to anybody. To apply, please fill this application form https://cvent.me/xqlq0G preferably no later than March 27, 2020. 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 Yale 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] Final Announcement: Second DeepSpec Summer School
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] [Application deadline: March 23rd] 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 and Verifiable C: a logic and toolset for Lennart Beringer proving C programs correct Adam ChlipalaImplementing, specifying, verifying, and compiling hardware components with Kami Zach Tatlock Verifying distributed systems Benjamin Pierce Property-based random testing with QuickChick All DeepSpec PIs Towards 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] 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] ITP2012: call for participation
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Differences to preliminary call: - Registration is now open, for conference and associated workshops - Reservation for student dorm rooms now open (part of registration) - Technical Program now available on the web page - 3rd International Conference on Interactive Theorem Proving August 13 - 15, 2012, Princeton, NJ itp2012.cs.princeton.edu with colocated workshops on Coq and Isabelle on August 12th. Registration is now available via the conference web page, including the option to book accommodation in a student dormitory. See below for fees etc. Highlights of the conference: - - Pre-conference reception Sunday, August 12th; open to conference and workshop participants. - Start of technical program: 9am, Monday August 13th - 3 invited speakers: Gilles Barthe (IMDEA Madrid): Computer-aided Cryptographic Proofs Larry Paulson (Cambridge): MetiTarski: Past and Future Andre Platzer (CMU): Differential Dynamic Logic and Differential Invariants for Hybrid Systems - Tutorial on Abella by Andrew Gacek (Rockwell Collins) - 21 technical papers, 4 rough diamonds - Outdoor event: canoeing/kayaking on the Delaware Raritan Canal - BBQ at the shore of Carnegie Lake - End of conference: around 5pm, Wednesday August 15th - A detailed schedule of presentations is available on the conference web site Associated workshops (August 12): - Isabelle Users Workshop 2012 (www21.in.tum.de/~nipkow/Isabelle2012) The 4th Coq Workshop (coq.inria.fr/coq-workshop/2012) Accommodation options (please see conference web page for details): --- - Hotel: Nassau Inn (nassauinn.com): $135pppn + Tax, incl breakfast Booking is under the responsibility of the conference attendees. Please mention ITP 2012 when making a reservation to obtain the above rate. - Student Dormitory: Scully Hall: $60pppn incl breakfast. Room reservation is part of conference registration process. Travel (again see conference web page for details): --- We strongly recommend flying to/from Newark International Airport (Airport code: EWR). Other airports in the area (JKF, La Guardia, Philadelphia) are possible but significantly less convenient. Conference registration (follow Registration link on web page): --- Early registration fees (until July 22nd): Workshops only Conference Conference + WS Regular 100$ 350$ 400$ Student 70$ 200$ 250$ Registration after July 22nd: additional USD 50 in each category. The cancellation policy is outlined on the web page. Chairs -- Andrew Appel, Lennart Beringer, Amy Felty
[TYPES/announce] ITP'12: final call for workshop proposals
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] ITP 2012: Third Conference on Interactive Theorem Proving Princeton, NJ, August 13 - 16, 2012 Conference home page: itp2012.cs.princeton.edu Final call for workshop proposals Submission deadline: December 5th, 2012 The ITP conference series - The ITP conference series is concerned with all topics related to Interactive Theorem Proving, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and formalization of mathematics. The third ITP conference, ITP 2012, will be held at Princeton University, between August 13th and August 16th, 2012. Scope and organization of workshops --- Similar to previous iterations of the conference, researchers and practitioners are invited to submit proposals for colocated workshops on topics relating to interactive theorem proving. Workshops can target the ITP community in general, focus on a particular ITP system, or highlight more specific issues or recent developments. Proposals for in-depth tutorials or tool introductions are also welcome. All colocated events will precede the main conference, and will be held on university premises. Conference facilities (meeting rooms, standard technical equipment) are offered free of charge to the organizers; workshop-only attendees will enjoy a significantly reduced registration fee. Participants will be able to choose between hotel accommodation or accommodation in university dormitories, both in walking distance to the conference venue. Detailed organizational matters such as paper submission and review process, or publication of proceedings, are up to the organizers of individual workshops. All accepted workshops will be expected to have the programme ready by July 1st 2012. Format of proposals --- Proposals for workshops should contain at least the following pieces of information. - name and contact details of the main organizer(s) - names of additional organizers (optional) - title and organizational style of workshop (tutorial, public workshop, project workshop, etc) - preferred length of workshop (half day, full day etc) - estimated number of attendees - short (up to 1 page) description of topic - (if applicable) pointers to previous editions of the workshop, or to similar events Submission and notification details --- Proposals are invited to be submitted by email to itp2...@easychair.org, no later than December 5th, 2011. The workshop selection committee consists of the ITP chairs Andrew Appel, Princeton University Lennart Beringer, Princeton University Amy Felty, University of Ottawa. Selected workshops will be notified by January 9th, 2012.
[TYPES/announce] ITP 2012: Call for workshop proposals
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] ITP 2012: Third Conference on Interactive Theorem Proving Princeton, NJ, August 13 - 16, 2012 Conference home page: itp2012.cs.princeton.edu Call for workshop proposals The ITP conference series - The ITP conference series is concerned with all topics related to Interactive Theorem Proving, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and formalization of mathematics. The third ITP conference, ITP 2012, will be held at Princeton University, between August 13th and August 16th, 2012. Scope and organization of workshops --- Similar to previous iterations of the conference, researchers and practitioners are invited to submit proposals for colocated workshops on topics relating to interactive theorem proving. Workshops can target the ITP community in general, focus on a particular ITP system, or highlight more specific issues or recent developments. Proposals for in-depth tutorials or tool introductions are also welcome. All colocated events will precede the main conference, and will be held on university premises. Conference facilities (meeting rooms, standard technical equipment) are offered free of charge to the organizers; workshop-only attendees will enjoy a significantly reduced registration fee. Participants will be able to choose between hotel accommodation or accommodation in university dormitories, both in walking distance to the conference venue. Detailed organizational matters such as paper submission and review process, or publication of proceedings, are up to the organizers of individual workshops. All accepted workshops will be expected to have the programme ready by July 1st 2012. Format of proposals --- Proposals for workshops should contain at least the following pieces of information. - name and contact details of the main organizer(s) - names of additional organizers (optional) - title and organizational style of workshop (tutorial, public workshop, project workshop, etc) - preferred length of workshop (half day, full day etc) - estimated number of attendees - short (up to 1 page) description of topic - (if applicable) pointers to previous editions of the workshop, or to similar events Submission and notification details --- Proposals are invited to be submitted by email to itp2...@easychair.org, no later than December 5th, 2011. The workshop selection committee consists of the ITP chairs Andrew Appel, Princeton University Lennart Beringer, Princeton University Amy Felty, University of Ottawa. Selected workshops will be notified by January 9th, 2012.
