[TYPES/announce] Verification Mentorship Workshop 2021: Call for Participation

[Arjun Radhakrishna]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Verification Mentoring Workshop (VMW) 2021
http://i-cav.org/2021/mentoring/

co-located online with CAV 2021
18-19th July 2021

Call for Participation

Are you an undergraduate or a graduate student interested in computer aided 
verification and formal methods, but don't know where to start? Are you looking 
for advice and mentoring on doing research, on grad school and beyond? We 
invite you to participate in the Verification Mentoring Workshop (VMW) 2021.

VMW is co-hosted with Computer Aided Verification (CAV) 2021 and will be held 
online on July 18th and 19th 2021. The purpose of the Verification Mentoring 
Workshop is to provide mentoring and career advice to early-stage graduate 
students and late-stage undergraduate students, and introduce them to research 
topics aligned with the CAV conference and, more generally, formal methods. The 
workshop particularly encourages participation of women and underrepresented 
minorities.

The program for VMW 2021 includes a number of talks and interactive sessions. 
The technical talks will provide gentle introductions to several recurring 
research themes in CAV, while the mentoring talks will provide useful tips 
about how to do good research and how to communicate your research well. The 
program also includes a panel that will feature leading researchers in the 
field. More information can be found at http://i-cav.org/2021/mentoring/.

VMW will provide financial support to select students to cover the registration 
fees for VMW and the CAV conference. Interested students are encouraged to 
apply here before June 18th, 2021: https://forms.gle/acivSdF4P4Xkjm4u7.

Confirmed Speakers:
Christel Baier, TU Dresden
Chuchu Fan, MIT
Temesghen Kahsai, Amazon
Oded Padon, VMWare Research
Sukyoung Ryu, KAIST
Moshe Y. Vardi, Rice University

In case of questions, please contact the organizers:
Jean-Baptiste Jeannin, University of Michigan
Arjun Radhakrishna, Microsoft
Suguman Bansal, University of Pennsylvania
Caterina Urban, INRIA & École Normale Supérieure | PSL University
Roopsha Samanta, Purdue University

[TYPES/announce] Call for papers: HATRA (Human Aspects of Types and Reasoning Assistants)

[Michael Coblenz]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Programming language designers seek to provide strong tools to help developers 
reason about their programs. For example, the formal methods community seeks to 
enable developers to prove correctness properties of their code, and type 
system designers seek to exclude classes of undesirable behavior from programs. 
The security community creates tools to help developers achieve their security 
goals. In order to make these approaches as effective as possible for 
developers, recent work has integrated approaches from human-computer 
interaction research into programming language design. This workshop brings 
together programming languages, software engineering, security, and 
human-computer interaction researchers to investigate methods for making 
languages that provide stronger safety properties more effective for 
programmers and software engineers.

We have two goals: (1) to provide a venue for discussion and feedback on 
early-stage approaches that might enable people to be more effective at 
achieving stronger safety properties in their programs; (2) to facilitate 
discussion about relevant topics of participant interest.

HATRA is interested in two different kinds of contributions. First, extended 
abstracts that summarize an existing body of work that is relevant to the 
workshop’s topic; the presentations serve to familiarize the community, which 
may be diverse, with work that already exists. Second, research papers that 
describe a new idea, approach, or hypothesis in the space, and are presented as 
an opportunity for the authors to receive community feedback and for the 
community to seek inspiration from others.

The day will be divided into two segments. In the first segment, authors of 
accepted papers will present their work. In the second segment, we will conduct 
an “unconference”-style meeting. By allowing the participants to drive the 
agenda, we hope to focus on topics that provide stimulating and enlightening 
discussion.

HATRA welcomes two kinds of submissions:
• Extended abstracts summarizing existing published work that would be 
of interest to the community.
• Research proposals, position papers, and early-stage result papers. 
These come in short (up to four pages) and long (up to eight pages) varieties. 
These may describe hypotheses, ideas for research, or early-stage results. The 
objective is to provide an opportunity for the authors to receive feedback from 
the community as well as to help inspire participants to identify and clarify 
their own research directions. To encourage submission of ideas that may be 
published in other venues in the future, papers will not be published in the 
ACM Digital Library.

Topics of interest include, but are not limited to:
• Type system design
• Programming language evaluation
• Programming language and tool design methodology
• Interactive theorem provers
• Lightweight specification tools
• Proof engineering
• Psychology of programming

The submission deadline is August 6, 2021. For more information, please see the 
web site: https://2021.splashcon.org/home/hatra-2021 


Organizing Committee:
Michael Coblenz (University of Maryland)
Luke Church (University of Cambridge)
Chris Martens (North Carolina State University)


Program Committee:
Will Crichton (Stanford University)
Jonathan Edwards
Molly Feldman (Williams College)
Andrew Head (UC Berkeley)
Alan Jeffrey (Roblox)
Shriram Krishnamurthi (Brown University)
Niek Mulleners (Utrecht University)
Cyrus Omar (University of Michigan)
Peter-Michael Osera (Grinnell College)
Hila Peleg (Technion Israel Institute of Technology)
Alastair Reid (Google Research)
Tianyi Zhang (Harvard University)

[TYPES/announce] Postdoc position at Cambridge in programming with equations

[Jeremy Yallop]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

We have an opening in Cambridge for a researcher on the Frex project
(https://www.cl.cam.ac.uk/~jdy22/projects/frex).  Informal enquiries
are welcome: please feel free to get in touch.

---
Research Assistant / Associate in Programming with Equations (Fixed Term)
https://www.jobs.cam.ac.uk/job/29773/

Applications are invited for a Research Assistant/Associate to join
the Frex project.

The Frex project investigates the use of equations in programming.
There is often a large gap between what programmers know about their
programs and what compilers are able to deduce.  Frex targets this gap
by exposing to the compiler the equations proved by programmers about
programs so that they can be used to improve optimisation and type
checking.

The position will involve working with Frex project members at the
Universities of Cambridge, Edinburgh and St Andrews to extend and
improve the design and implementations of Frex. Work up to this point
has focused on equations for first-order single-sorted algebras and we
plan to extend the techniques to more elaborate settings.

The successful candidate is likely to have (or expect to be awarded
soon) a PhD in computer science or a related discipline, as well as a
track record of published research and experience or demonstrable
interest in some combination of the following:

- Dependently typed programming languages or proof assistants based on
type theory (e.g. Agda, Idris, Coq, Lean)

- Functional programming languages (e.g. F#, OCaml, Haskell)

- Partial evaluation, normalization by evaluation, multi-stage
programming, supercompilation or related techniques

- Algebraic structures, universal algebra and categorical algebra

Informal enquiries are welcome and should be directed to Dr Jeremy
Yallop (jeremy.yal...@cl.cam.ac.uk)

Expected starting date: 1 September 2021

[TYPES/announce] Expression of Interest for MSCA PF on Reversible Computing @ UNIBO, Italy

[ivan.lanese]

[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Dear all,
 University of Bologna (Italy) is encouraging young researchers to
apply for a MSCA Postdoctoral Fellowships with University of Bologna
as host institution. All information on MSCA Postdoctoral Fellowships can 
be found at:


https://ec.europa.eu/research/mariecurieactions/actions/postdoctoral-fellowships

I am particularly interested in supervising future applicants (and
work with them towards an application) in the area of reversible
computing and reversible debugging. Reversible computing allows a
program to execute both forward and backward, and it found a natural
application in the exploration of an execution forward and backward
looking for a bug. The technique is used in mainstream debuggers such
as GDB and WinDBG.

If you are interested or would like to have more information feel free
to contact me.

Best,

Ivan Lanese

[TYPES/announce] CFP: GandALF2021 - 12th International Symposium on Games, Automata, Logics, and Formal Verification

[Davide Bresolin]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

*
CALL FOR PAPERS - GandALF 2021
*
The 12th International Symposium on Games, Automata, Logics, and Formal 
Verification will be held in Padua (Italy) on September 20-22, 2021.

This year, GANDALF will be organised together with the 3rd Workshop on 
Artificial Intelligence and fOrmal VERification, Logic, Automata, and sYnthesis 
(OVERLAY 2021, https://overlay.uniud.it/workshop/2021/). The OVERLAY workshop 
focuses on the relationships between Artificial Intelligence and Formal 
Methods, and discusses on the opportunities and challenges at the border of the 
two areas. Both events will be hosted by the University of Padua, and will 
share some invited speakers. We encourage participation in both events.

GANDALF 2021 is planned to be a hybrid conference. We aim at organizing an 
in-presence event, but there will be possibilities for virtual participation 
for delegates affected by travel restrictions.

https://gandalf2021.math.unipd.it/

*
The aim of GandALF 2021 is to bring together researchers from academia and 
industry which are actively working in the fields of Games, Automata, Logics, 
and Formal Verification. The idea is to cover an ample spectrum of themes, 
ranging from theory to applications, and stimulate cross-fertilization. Papers 
focused on formal methods are especially welcome. Authors are invited to submit 
original research or tool papers on all relevant topics in these areas. Papers 
discussing new ideas that are at an early stage of development are also 
welcome. The topics covered by the conference include, but are not limited to, 
the following:

Automata Theory
Automated Deduction
Computational aspects of Game Theory
Concurrency and Distributed computation
Decision Procedures
Deductive, Compositional, and Abstraction Techniques for Verification
Finite Model Theory
First-order and Higher-order Logics
Formal Languages
Formal Methods for Systems Biology, Hybrid, Embedded, and Mobile Systems
Games and Automata for Verification
Game Semantics
Logical aspects of Computational Complexity
Logics of Programs
Modal and Temporal Logics
Model Checking
Models of Reactive and Real-Time Systems
Probabilistic Models (Markov Decision processes)
Program Analysis and Software Verification
Reinforcement Learning
Run-time Verification and Testing
Specification and Verification of Finite and Infinite-state Systems
Synthesis

IMPORTANT DATES (all dates are AoE)
*
Abstract submission: June 23, 2021
Paper submission: June 30, 2021
Notification: July 30, 2021
Camera-ready: August 30, 2021
Conference: September 20-22, 2021

PUBLICATIONS
*
The proceedings will be published by Electronic Proceedings in Theoretical 
Computer Science.

***Authors of the best papers will be invited to submit a revised version of 
their work to a special issue of Logical Methods in Computer Science***.

The previous editions of GandALF already led to special issues of the 
International Journal of Foundations of Computer Science (GandALF 2010), 
Theoretical Computer Science (GandALF 2011 and 2012), Information and 
Computation (GandALF 2013, 2014, 2016, 2017, 2019 and 2020), and Acta 
Informatica (GandALF 2015).

SUBMISSIONS
*
Submitted papers should not exceed 14 pages (excluding references and clearly 
marked appendices) using EPTCS format, be unpublished and contain original 
research. Please use the LaTeX style provided at http://style.eptcs.org to 
format the paper. For papers reporting experimental results, authors are 
encouraged to make their data available with their submission. Submissions must 
be in PDF format and will be handled via the EasyChair Conference system at the 
following address:

https://www.easychair.org/conferences/?conf=gandalf2021

INVITED SPEAKERS
*
Roderick Bloem, TU Graz, Austria
Anca Muscholl, LaBRI, Bordeaux, France
Nicola Olivetti, Aix-Marseille University, France
S.E. (Sicco) Verwer, TU Delft, The Netherlands

PROGRAM CHAIRS
*
Davide Bresolin, University of Padua (Italy)
Pierre Ganty, IMDEA Software Institute, Madrid (Spain)

PROGRAM COMMITTEE
*
Mohamed Faouzi Atig, Uppsala University (Sweden)
Christel Baier, TU Dresden (Germany)
Saddek Bensalem, VERIMAG (France)
Nathalie Bertrand, INRIA (France)
Pedro Cabalar,