[TYPES/announce] Call for participation: 1st Rust Verification Workshop
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] 1st Rust Verification Workshop Online, co-located with ETAPS 2021 April 07, 09, and 12, 2021, 16:00 - 18:10 GMT https://sites.google.com/view/rustverify2021 Rust is a new programming language for writing performant code with strong type and memory safety guarantees. It is now considered a serious alternative to C and C++ for systems programming, because it provides high-level abstractions but without the cost of garbage collection. Given the growing popularity of Rust, and given that bugs in systems programs can be costly, there is growing interest in the program verification community for building program verifiers for Rust. In this workshop, we aim to bring together language designers, application developers and formal verification tool builders, to exchange ideas and build collaborations around developing verified Rust programs. The goal of this workshop is to bring researchers from a variety of different backgrounds and perspectives together to exchange new and exciting ideas concerning the verification of Rust programs and exploring avenues for collaboration. The program will contains a combination of invited talks and contributed talks. A detailed schedule is available here: https://sites.google.com/view/rustverify2021. Registration Please register via ETAPS at https://etaps.org/2021/registration. You will receive access information once you have registered. Organizers: * Rajeev Joshi, Amazon Web Services * Nicholas Matsakis, Amazon Web Services * Peter Müller, ETH Zurich
[TYPES/announce] PhD Position in Programming Languages at TU Delft
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dear all, I have an opening for a 4 year PhD position in the Programming Languages Group at Delft University of Technology. The PhD position is about defining and implementing typed programming languages in a modular way. The ideal candidate will have experience with one or more of the following topics: - functional programming - monads and/or algebraic effects and handlers - programming language engineering (interpreters/compilers/type checkers/...) The full ad (link below) contains suggestions for topics that can be explored as part of the PhD. But the topic is not limited to the suggestions in the ad. Get in touch if you are interested in doing research on defining and implementing typed programming languages, modularly. https://www.academictransfer.com/en/298133/phd-position-dynamic-semantics-specification/ The deadline for application is 2 June 2021, and the ideal start date is around September. Best regards, Casper Bach Poulsen Assistant Professor, Delft University of Technology http://casperbp.net
[TYPES/announce] FMBC 2021 - Call for Papers
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] [ Please distribute, apologies for multiple postings. ] 3rd International Workshop on Formal Methods for Blockchains (FMBC) - First Call https://fmbc.gitlab.io/2021 July 18 or 19 (TBA), 2021 Co-located with the 33nd International Conference on Computer-Aided Verification (CAV 2021) http://i-cav.org/2021/ - IMPORTANT DATES Abstract submission: April 22, 2021 Full paper submission: April 29, 2021 Notification: June 10, 2021 Camera-ready: July 8, 2021 Workshop: July 18 or 19 (TBA), 2021 Deadlines are Anywhere on Earth: https://en.wikipedia.org/wiki/Anywhere_on_Earth TOPICS OF INTEREST Blockchains are decentralized transactional ledgers that rely on cryptographic hash functions for guaranteeing the integrity of the stored data. Participants on the network reach agreement on what valid transactions are through consensus algorithms. Blockchains may also provide support for Smart Contracts. Smart Contracts are scripts of an ad-hoc programming language that are stored in the Blockchain and that run on the network. They can interact with the ledger’s data and update its state. These scripts can express the logic of possibly complex contracts between users of the Blockchain. Thus, Smart Contracts can facilitate the economic activity of Blockchain participants. With the emergence and increasing popularity of cryptocurrencies such as Bitcoin and Ethereum, it is now of utmost importance to have strong guarantees of the behavior of Blockchain software. These guarantees can be brought by using Formal Methods. Indeed, Blockchain software encompasses many topics of computer science where using Formal Methods techniques and tools are relevant: consensus algorithms to ensure the liveness and the security of the data on the chain, programming languages specifically designed to write Smart Contracts, cryptographic protocols, such as zero-knowledge proofs, used to ensure privacy, etc. This workshop is a forum to identify theoretical and practical approaches of formal methods for Blockchain technology. Topics include, but are not limited to: * Formal models of Blockchain applications or concepts * Formal methods for consensus protocols * Formal methods for Blockchain-specific cryptographic primitives or protocols * Design and implementation of Smart Contract languages * Verification of Smart Contracts SUBMISSION Submit original manuscripts (not published or considered elsewhere) with a page limit of 12 pages for full papers and 6 pages for short papers (excluding bibliography and short appendix of up to 5 additional pages). Alternatively you may also submit an extended abstract of up to 3 pages (including bibliography) summarizing your ongoing work in the area of formal methods and blockchain. Authors of selected extended-abstracts are invited to give a short lightning talk. Submission link: https://easychair.org/conferences/?conf=fmbc2021 Authors are encouraged to use LaTeX and prepare their submissions according to the instructions and styling guides for OASIcs provided by Dagstuhl. Instructions for authors: https://submission.dagstuhl.de/documentation/authors#oasics At least one author of an accepted paper is expected to present the paper at the workshop as a registered participant. PROCEEDINGS All submissions will be peer-reviewed by at least three members of the program committee for quality and relevance. Accepted regular papers (full and short papers) will be included in the workshop proceedings, published as a volume of the OpenAccess Series in Informatics (OASIcs) by Dagstuhl. INVITED SPEAKER To be confirmed PROGRAM COMMITTEE PC CO-CHAIRS * Bruno Bernardo (Nomadic Labs, France) (br...@nomadic-labs.com) * Diego Marmsoler (University of Exeter, UK) (d.marmso...@exeter.ac.uk) PC MEMBERS To be confirmed
[TYPES/announce] OPLSS 2021 - Oregon Programming Languages Summer School
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] We are pleased to announce the program of the 19th annual Oregon Programming Languages Summer School (OPLSS) to be held *online* from June 14th to June 26th, 2021. The theme for this year is "Foundations of Programming and Security." The registration deadline is April 30th, 2021. Full information on registration can be found here: https://www.cs.uoregon.edu/Activities/summerschool This year, OPLSS will be a little different. The registration rates have been updated to reflect the fact that OPLSS will be fully virtual. In consideration of the current circumstances, there are now three categories for registration: * Students & Postdocs: Free * Professors & Industrial Professionals: $250 * Others: For those for which the professional registration fee would pose an economic burden, please contact us for more details. Some examples include: people on temporary hiatus due to the pandemic; unemployed or retired professionals. To help the online lectures and discussion sessions run smoothly, we request volunteers to contribute to one of these roles: * Scribe: Prepare written notes for certain lectures. * Lecture assistant: Gather & relay questions to the speaker. Please contact us during registration to indicate your interest in one of these roles. The speakers and topics include: Stephanie Balzer — Carnegie Melon University Session-Typed Concurrent Programming Ugo Dal Lago — University of Bologna >From Program Equivalences to Program Metrics Robert Harper — Carnegie Melon University Principles of Programming Languages Justin Hsu — University of Wisconsin–Madison Reasoning about Probabilistic Programs Patricia Johann — Appalachian State University Semantics of Advanced Data Types Alejandro Russo — Chalmers University Information-flow Control Libraries Alexandra Silva — University College London Kleene Algebras and Applications Nikhil Swamy — Microsoft Research Proof-oriented Programming in F* Tarmo Uustalu — Reykjavik University Monads and Interaction More information about these topics can be found at: https://www.cs.uoregon.edu/research/summerschool/summer21/topics.php We hope you can join us for this excellent program! Zena Ariola, Marco Gaboardi, and Paul Downen [image: OPLSS_Logo.png]
