[TYPES/announce] Research Fellow at UCL - Programming Principles, Logic, and Verification

[James Brotherston]

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


Research Fellow - Programming Principles, Logic and Verification

University College London

The Interface Reasoning for Interacting Systems (IRIS) project, led by 
Prof. David Pym (UCL), seeks to understand the compositional structure 
of systems and their communications, at all scales from computer code 
through distributed systems to organizational structure. We are seeking 
a Research Fellow to join our team and conduct theoretical and/or 
applicable research in this area.


The research programme will be in the broad area of *verification* from 
the perspective of the IRIS project.  We seek candidates with a PhD in 
computer science or a closely related area and an interest in any or all 
of the following:


 * program analysis and verification;
 * concurrency theory;
 * probability theory;
 * automated reasoning;
 * logic and formal methods.

Previous experience in developing automated software tools is desirable, 
but not essential.


The role will be jointly managed by James Brotherston (and David Pym) at 
UCL and John Wickerson at Imperial College. While based primarily at 
UCL, the role will involve frequent contact with Imperial College and 
the other project partners.


The post is offered for 12 months initially, but is extensible up to 36 
months.


Informal enquiries prior to application are welcome and should be 
directed initially to James Brotherston at j.brothers...@ucl.ac.uk.


Apply at:  https://tinyurl.com/yctdne4y

More info on IRIS at: https://interfacereasoning.com/

[TYPES/announce] Chalmers Online Functional Programming Seminar Series (TODAY: Benjamin Pierce!)

[Benjamin C. Pierce]

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

A reminder of today's seminar by Benjamin Pierce. 16.00.
Backtracking Generators for Random Testing.

Last week we had 720 people who tuned in to Simon Peyton Jones! Unfortunately, 
we had severe problems using Zoom webinar technology (which was dimensioned in 
our license for up to 1000 people, but Zoom was just not up to the task).

This week we will use YouTube Live streaming and sli.do for questions. All 
relevant links are on chalmersfp.org . See you there!

Mary Sheeran, John Hughes, and Koen Claessen

[TYPES/announce] FTfJP 2020 (virtual): Second CFP

[Oortwijn Wytse]

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

# SECOND CALL FOR PAPERS

Submission deadline: Friday 5 June (AoE)

22st Workshop on Formal Techniques for Java-like Programs (FTfJP 2020)
https://2020.ecoop.org/track/FTfJP-2020-papers

FTfJP will be virtual this year and is expected to be in mid July.


## About FTfJP 2020 (virtual)

Formal techniques can help analyse programs, precisely describe
program behaviour, and verify program properties. Modern programming
languages are interesting targets for formal techniques due to their
ubiquity and wide user base, stable and well-defined interfaces and
platforms, and powerful (but also complex) libraries. New languages
and applications in this space are continually arising, resulting in
new programming languages (PL) research challenges.

Work on formal techniques and tools and on the formal underpinnings of
programming languages themselves naturally complement each
other. FTfJP is an established workshop which has run annually since
1999 alongside ECOOP, with the goal of bringing together people
working in both fields.

The workshop has a broad PL theme; the most important criterion is
that submissions will generate interesting discussions within this
community. The term “Java-like” is somewhat historic and should be
interpreted broadly: FTfJP solicits and welcomes submission relating
to programming languages in general, beyond Java, C#, Scala, etc.

Example topics of interest include:

* Language design and semantics
* Type systems
* Concurrency and new application domains
* Specification and verification of program properties
* Program analysis (static or dynamic)
* Program synthesis
* Security
* Pearls (programs or proofs)

FTfJP welcomes submissions on technical contributions, case studies,
experience reports, challenge proposals, and position papers.


## Submissions

Contributions are sought in two categories:

* Full Papers (6 pages, excluding references) present a technical
  contribution, case study, or detailed experience report. We welcome
  both complete and incomplete technical results; ongoing work is
  particularly welcome, provided it is substantial enough to stimulate
  interesting discussions.

* Short Papers (2 pages, excluding references) should advocate a
  promising research direction, or otherwise present a position likely
  to stimulate discussion at the workshop. We encourage
  e.g. established researchers to set out a personal vision, and
  beginning researchers to present a planned path to a PhD.

Both types of contributions will benefit from feedback received at the
workshop. Submissions will be peer reviewed, and will be evaluated
based on their clarity and their potential to generate interesting
discussions. The format of the workshop encourages interaction. FTfJP
is a forum in which a wide range of people share their expertise, from
experienced researchers to beginning PhD students.


## Formatting and Publication

Submissions should be in acmart/sigplan style, 10pt font. Formatting
requirements are detailed on the SIGPLAN Author Information page
(https://www.sigplan.org/Resources/Author).

Accepted papers will be published in the ACM Digital Library by
default, though authors will be able to opt out of this publication,
if desired. At least one author of an accepted paper must attend the
workshop to present the work and participate in the discussions.


## Important Dates

* Submission: June 5th (AoE)
* Notification: July 3th


## Program Committee

* Wolfgang Ahrendt (Chalmers University, Sweden)
* Petra van den Bos (University of Twente, the Netherlands)
* Marie Farrell (University of Liverpool, UK)
* Paula Herber (University of Munster, Germany)
* Nikolai Kosmatov (CEA LIST, France)
* James Noble (Victoria University of Wellington, New Zealand)
* Violet Ka I Pun (University of Oslo, Norway)
* John Singleton (University of Central Florida, USA)
* Mattias Ulbrich (KIT, Germany)
* Anton Wijs (Eindhoven University, the Netherlands)
* Elena Zucca (University of Genova, Italy)

[TYPES/announce] postdoc position in Aarhus, Denmark, at Center for Basic Research in Program Verification

[Lars Birkedal]

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


We are looking for Postdocs to work in the Center for Basic Research in Program 
Verification
in Aarhus, Denmark. Research topics include: extensions of higher-order 
concurrent
separation logics (such as our Iris logic, see iris-project.org), e.g., to 
reason about
distributed systems; probabilistic program logics; logical relations for 
relational reasoning
about safety and security properties; formal modeling of low-level capability 
machines,
and secure compilation; guarded cubical type theory; and Coq formalizations.
The Post Doc positions are for two years (with a possibility of extension).

Application deadline is June 1, 2020.

See 
https://www.au.dk/om/stillinger/job/center-for-basic-research-in-program-verification-cpv-is-looking-for-postdocs/
for more information.

Please contact me at birke...@cs.au.dk if you have 
any questions.

Best wishes,
Lars Birkedal


-- --
Lars Birkedal
Villum Investigator
Professor, Head of Logic and Semantics Group
Dept. of Computer Science
Aarhus University
Aabogade 34
8200 Aarhus N
Denmark
birke...@cs.au.dk
www.cs.au.dk/~birke