[TYPES/announce] Proof and Computation 2021

[Chuangjie Xu]

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

[Apologies for multiple postings.]

Autumn school "Proof and Computation"
Online, 13th and 14th September 2021
http://www.mathematik.uni-muenchen.de/~schwicht/pcv21.php

This year's autumn school "Proof and Computation" will be held as an online
workshop from 13th to 14th September 2021.

SCOPE

- Predicative Foundations
- Constructive Mathematics and Type Theory
- Computation in Higher Types
- Extraction of Programs from Proofs

TALKS

- Liron Cohen: Effectful Proving (and Disproving)
- David Corfield: Modal Type Theories
- Grigory Devadze: Computer-certified proofs for control theoretic aspects
  and program extraction
- Dominik Kirst: Formalising Metamathematics in Constructive Type Theory
- Klaus Mainzer: Proof and Computation: Perspectives of Mathematics,
  Computer Science, and Philosophy
- Antonio Piccolomini d'Aragona: Epistemic grounding. Semantics and
  calculi based on Prawitz's theory of grounds
- Sebastian Posur: On free abelian categories for theorem proving
- Florian Steinberg: Continuity, computability and discreteness
- Holger Thies: Complexity Theory in Analysis with Applications to
  Differential Equations

REGISTRATION

If you are interested in participating, please write to Nils Köpp
(ko...@math.lmu.de) to receive the Zoom link.


The workshop is supported by the Udo Keller Stiftung (Hamburg) and the CID
(Computing with Infinite Data) programme of the European Commission.


Klaus Mainzer
Peter Schuster
Helmut Schwichtenberg


This message was sent using IMP, the Internet Messaging Program.

[TYPES/announce] three-year postdoc position on verifying concurrent programs

[Gardner, Philippa A]

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

Hello all,

[Apologies for multiple postings.]

I have a  three-year post-doctoral research position available  on `Gillian: 
Concurrency’, as part of a wider project on the Gillian platform for unified 
compositional symbolic reasoning about program correctness and incorrectness. 
It could turn into a more theoretical or more practical project depending on 
the strengths of the successful applicant.

DEADLINE:  15th August  2021, flexible start date in 2022 (or earlier if you 
wish).

The Gillian project  is currently funded by my national fellowship on `Verified 
Trustworthy Software Specification’ and a large Facebook gift. Details of this 
project  are given below and details about my research group in general can be 
found here. I have further flexible funding so 
please get in touch if the timing for you is not quite right.

If you are interested, please do not hesitate to contact me, cc’ing my 
administrator Teresa Carbajo Garcia,
t.carbajo-gar...@imperial.ac.uk.

Best wishes,
Philippa
---

Professor Philippa Gardner FREng
Department of Computing
Imperial College
180 Queen’s Gate
London
SW7 2AZ

Your working day may not be the same as mine. Please do not feel
obliged to reply to this email outside your normal working hours.

---

Gillian: Concurrency

Gillian [1,2] is a multi-language platform for unified compositional symbolic 
reasoning about program correctness and incorrectness. It is underpinned by a 
core symbolic execution engine, parametric on the memory model of the target 
language, with strong mathematical foundations that unifies symbolic testing 
and verification. Gillian has been instantiated to JavaScript and C, obtaining 
results on real-world AWS code that demonstrate the viability of our unified, 
parametric approach.

Gillian  currently works on sequential programs. This project will extend the 
core of Gillian with concurrency. A more theoretical project will develop a 
Gillian instantiation for a small concurrent While language and explore 
different types of concurrency reasoning for different types of strong and weak 
memory models, both theoretically and with Gillian. A more practical project 
will develop a Gillian instantiation for concurrent Rust, building on the 
current development of a Gillian instantiation for sequential Rust, and explore 
symbolic testing and verification for real-world Rust programs. The spirit of 
the group is to get the best fit between people and research, so there is much 
flexibility with these projects.

We have recently developed a general infrastructure for the symbolic analysis 
of event-driven web applications [3]. I have also worked for many years on the 
compositional reasoning about concurrent programs, introducing fundamental 
techniques which underpin modern concurrent separation logics [4,5] and working 
on  weak consistency models for atomic distributed transactions [6]. Some of 
this experience will inform the choices for extending Gillian with concurrency, 
but we will start from the beginning working out what are the right first 
choices for the project.

References

[1] Gillian, Part 1: A Multi-language Platform for Symbolic Execution, Jose 
Fragoso Santos, Petar Maksimovic, Sacha-Elie Ayoun and Philippa Gardner, 
PLDI'20. Talks at Rebase at ECOOP/OOPSLAFaceTAV and
Amazon in 2020.

[2] Gillian, Part 2: Real-world Verification for JavaScript and C, Petar 
Maksimovic, Sacha-Elie Ayoun, Jose Fragoso Santos and Philippa Gardner, CAV’21, 
draft available upon request. Talks at Galois and Collège de France in 2021.

[3] A Trusted Infrastructure for Symbolic Analysis of Event-driven Web 
Applications, Gabriela Sampaio, Jose Fragoso Santos, Petar Maksimovic and 
Philippa Gardner, ECOOP’20.

[4] A Perspective on Specifying and Verifying Concurrent Modules, Thomas 
Dinsdale-Young, Pedro da Rocha Pinto and Philippa Gardner, Journal of Logical 
and Algebraic Methods in Programming, 2018.

[5] TaDA Live: Compositional Reasoning for Termination of Fine-grained 
Concurrent Programs, Emanuele D’Osualdo, Azadeh Farzan, Philippa Gardner and 
Julian Sutherland, TOPLAS 2021, draft available upon request.

[6] Data Consistency in Transactional Storage Systems: a Centralised Approach, 
Shale Xiong, Andrea Cerone, Azalea Raad and Philippa Gardner, ECOOP'20.

[TYPES/announce] Postdoctoral position at Stanford Center for AI Safety

[Clark Barrett]

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

The Stanford Center for AI Safety is sponsoring a new postdoctoral
fellowship position for Fall 2021.  Topics of interest include formal
methods applied to AI systems.  Details can be found on the center's
website at aisafety.stanford.edu.

Clark Barrett
Co-director, Stanford Center for AI Safety

[TYPES/announce] 6-Month postdoc in lambda-calculi and effects, University of Bath

[Willem Heijltjes]

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

We invite applications for a post-doctoral research position, to investigate a 
new approach to efficient computation with and without computational effects in 
the lambda-calculus.

This is a 6-month fixed-term role starting as soon as possible. It is part of 
the EPSRC-funded project `Typed Lambda-Calculi with Sharing and Unsharing'.

  To apply:   http://www.bath.ac.uk/jobs/Vacancy.aspx?ref=CC8432

  Enquiries:  w.b.heijlt...@bath.ac.uk

  Deadline:   27 July 2021

The project revolves around new ideas in lambda-calculus and functional 
programming, focused in two areas. The first is *computational effects*, where 
the project has developed a simple and natural approach that subsumes many 
existing efforts, called the Functional Machine Calculus (FMC). The second is 
*efficient computation*, which combines ideas from proof theory and optimal 
reduction to investigate new, refined type systems for the lambda-calculus.

The background and the source of original ideas is a branch of proof theory 
called "deep inference", which is closely related to category theory. Knowledge 
of this area is not essential to the advertised role.

We are looking for excellent candidates with a PhD (or expected to complete one 
soon) and a proven track record in one or more of the following areas:
 * Lambda-calculus
 * Functional programming theory
 * Computational effects
 * Semantics of programming
 * Deep-inference proof theory

As the successful candidate, you would contribute to one of several potential 
tasks, for example: 
 * expanding the FMC to a prototype functional language
 * investigating new type systems for the FMC
 * investigating efficient implementations of the FMC
 * further develop type systems towards optimal reduction

You will be part of the Mathematical Foundations group in the Department of 
Computer Science. We are a small, lively research group with an excellent 
international reputation. Some of our members are:
  Alessio Guglielmi  http://alessio.guglielmi.name
  Willem Heijltjes   http://willem.heijltj.es
  Jim Laird  http://researchportal.bath.ac.uk/en/persons/james-laird
  Guy McCusker   http://researchportal.bath.ac.uk/en/persons/guy-mccusker
  Thomas Powell  http://t-powell.github.io

Present circumstances permitting, you will have the opportunity to travel to 
various collaborators on the project in Europe, for example in Bologna and 
Paris.

The University of Bath is a top-ranking university and a great place to work. 
Bath is a Unesco World Heritage city with fantastic amenities offering 
excellent quality of life.

Links:

  Job advert:
 http://www.bath.ac.uk/jobs/Vacancy.aspx?ref=CC8432

  Typed Lambda-Calculi with Sharing and Unsharing:
 http://willem.heijltj.es/Unsharing

  Mathematical Foundations Group:
 http://www.bath.ac.uk/projects/mathematical-foundations-of-computation/

  Department of Computer Science:
 http://www.bath.ac.uk/departments/department-of-computer-science/