The Coq mailing list

[Jules Jacobs <julesjacobs AT gmail.com>]

Dear all,

On June 24, a Mini PL workshop will take place at Radboud University, organized by Robbert Krebbers.

The workshop features speakers Ralf Jung, Silvia Ghilezan, and Jorge Perez.

These speakers are also part of my PhD defense committee, which will take place after the workshop.

Program for the day:

- 12:00-13:00 Lunch

- 13:00-13:40 Ralf Jung: MiniRust: A complete, precise, executable, accessible, and

authoritative core language for Rust

- 13:40-14:20 Silvia Ghilezan: Probabilistic reasoning: computation vs types

- 14:20-15:00 Jorge Perez: Asynchronous Session-Based Concurrency: Deadlock-freedom in Cyclic Process Networks

- 15:00-15:30 Coffee

- 15:30-16:00 Walk to auditorium

- 16:30-17:30 PhD defense

Abstracts for the talks are included below.

The workshop will take place in the Mercator-I building (https://www.ru.nl/over-ons/de-campus/gebouwen-en-ruimtes/mercator-i) and the defense will take place in the Aula's auditorium (https://www.ru.nl/over-ons/de-campus/gebouwen-en-ruimtes/aula).

If you would like to attend, please register here before June 12: https://forms.gle/4kKMdgDDxHsmGKar6

Best regards,

Jules Jacobs

# Talks

TITLE: MiniRust: A complete, precise, executable, accessible, and

authoritative core language for Rust

SPEAKER: Ralf Jung, ETH Zurich

ABSTRACT: Real-world programming languages often suffer from notorious

under-specification. This is a particularly bad problem for languages

like C and C++ that make heavy use of Undefined Behavior (UB), as that

fundamentally prevents using testing to discover the specification: when

a program has UB, it may have arbitrary runtime behavior, so no

conclusion can be drawn from the results of such a test. While C and C++

do come with extensive specifications, these are written in plain

English in an axiomatic style, making them hard to interpret.

Rust is a modern language with a strong focus on safety and reliability.

However, to enable programmers to eek out every last bit of performance,

Rust also allows "unsafe code" where safety can no longer be guaranteed

by the compiler -- in unsafe Rust, Undefined Behavior is possible. Rust

therefore needs a specification which ensures that programmers and

compiler writers agree on what is and is not Undefined Behavior.

In this talk I will present my work-in-progress project MiniRust, a core

language for Rust. MiniRust aims to be complete, precise, executable,

accessible, and authoritative: the goal is to be able to cover all of

Rust via a lowering step that expands Rust into MiniRust, to define

language behavior unambiguously, to provide a reference interpreter that

can be used to test the specification and as a test oracle for language

implementations, and to be accessible to Rust developers. MiniRust is

currently being considered for inclusion in the authoritative Rust

specification.

---------------

TITLE: Probabilistic reasoning: computation vs types

SPEAKER: Silvia Ghilezan, University of Novi Sad & Mathematical

Institute of the Serbian Academy of Sciences and Arts

ABSTRACT: Reasoning with uncertainty has gained an important role in

logic, computer science, artificial intelligence and cognitive science.

There has been a growing interest in probabilistic reasoning about

proofs and programs. There are various ways to introducing

nondeterminism and probability to formal calculi. We will discuss two

different approaches: the computation in the presence of uncertainty and

probabilistic reasoning about typing. The former is currently the main

stream approach, whereas the later, which is in our focus, is a

combination of probabilistic logic and typed lambda calculus.

--------------

TITLE: Asynchronous Session-Based Concurrency: Deadlock-freedom in

Cyclic Process Networks

SPEAKER: Jorge Perez, University of Groningen

ABSTRACT: In this talk, I discuss recent work aimed at tackling the

challenge of ensuring the deadlock-freedom property for message-passing

processes that communicate asynchronously in cyclic process networks.

I shall present two contributions. First, I will present Asynchronous

Priority-based Classical Processes (APCP), a session-typed process

framework that supports asynchronous communication, delegation, and

recursion in cyclic process networks. Building upon the Curry-Howard

correspondences between linear logic and session types, APCP enjoys

essential properties, most notably deadlock-freedom. Second, I will

present and illustrate a new concurrent λ-calculus with asynchronous

session types, dubbed LAST^n. I will illustrate a precise technical

connection between APCP and LAST^n, namely how to soundly transfer the

deadlock-freedom guarantee from APCP to LAST^n.

(joint work with Bas van den Heuvel - https://arxiv.org/abs/2111.13091)