Scottish Programming Languages Seminar

Abstract

Hide Abstract

We adapt Fiore, Plotkin, and Turi’s treatment of abstract syntax with binding, substitution, and holes to account for languages with second-class sorts. These situations include programming calculi such as the Call-by-Value 𝜆-calculus (CBV) and Levy’s Call-by-Push-Value (CBPV). Prohibiting second-class sorts from appearing in variable contexts means the presheaf of variables is no longer a left-unit for Fiore et al’s substitution tensor product. We generalise their development to accommodate second-class sorts, and reuse much of the development through bicategorical arguments. We apply the resulting theory by proving substitution lemmata for varieties of CBV modularly.

Joint work with Marcelo Fiore, Georg Moser, and Sam Staton.

Abstract

Hide Abstract

This talk is an extended practice talk for TYPES 2025 where I am reporting on work-in-progress that uses techniques inspired by constructive negation to reframe decision procedures as pairings of positive datatypes that cancel each other out.

Specifically, I will report my experiences in providing a library of positive decision procedures, and using these procedures when programming. I will also examine how being so positive in one’s negativity can be backported to report our decision procedure's negativity more positively.

Please see the extended abstract for more information.

Abstract

Hide Abstract

Gradual typing provides a model for when a legacy language with less precise types interacts with a newer language with more precise types. Casts mediate between types of different precision, allocating blame when a value fails to conform to a type. The blame theorem asserts that blame always falls on the less-precisely typed side of a cast. One instance of interest is when a legacy language (such as Java) permits null values at every type, while a newer language (such as Scala or Kotlin) explicitly indicates which types permit null values. Nieto et al. in 2020 introduced a gradually typed calculus for just this purpose. The calculus requires three distinct constructors for function types and a non-standard proof of the blame theorem; it can embed terms from the legacy language into the newer language (or vice versa) only when they are closed. Here, we define a simpler calculus that is more orthogonal, with one constructor for function types and one for possibly nullable types, and with an entirely standard proof of the blame theorem; it can embed terms from the legacy language into the newer language (and vice versa) even if they are open. All results in the paper have been mechanized in Coq.

In addition to technical details, the talk will ponder a sociological question: why was Nieto et al 2020 was published in ECOOP, while our simpler solution was rejected from ESOP and went "straight to video" in JFP?

[Joint work with Ondrej Lhotak. Published in JFP 34, e15, doi:10.1017/S0956796824000121. Practice for a talk to be presented at ICFP 2025.]

Abstract

Hide Abstract

Actor languages such as Erlang and Elixir are widely used for implementing scalable and reliable distributed applications, but the informally-specified nature of actor communication patterns leaves systems vulnerable to costly errors such as communication mismatches and deadlocks. Multiparty session types (MPSTs) rule out communication errors early in the development process, but until now, the nature of actor communication has made it difficult for actor languages to benefit from session types.

This paper introduces Maty, the first actor language design supporting both static multiparty session typing and the full power of actors taking part in multiple sessions. Our main insight is to enforce session typing through a flow-sensitive type-and-effect system, combined with an event-driven programming style and first-class message handlers. Using MPSTs allows us to guarantee communication safety: a process will never send or receive an unexpected message, nor will it ever get stuck waiting for a message that will never arrive. We extend Maty to support both Erlang-style cascading failure handling and the ability to proactively switch between sessions. We implement Maty in Scala using an API generation approach, and evaluate our implementation on a series of microbenchmarks, a factory scenario, and a chat server.

Abstract

Hide Abstract

Concurrent programs destructively updating shared memory are notoriously hard to get right. Concurrent separation logics are logics with built-in notions of e.g. ownership of memory regions, concurrent accesses, and lock mechanisms. They give experts a way to verify a posteriori that complex concurrent imperative programs hopefully abide by their formal specification. We will see how next generation languages let us get rid of a posteriori verification in favour of a correct-by-construction approach whereby the program is interactively built in a specification-respecting dialogue with the compiler.

For this presentation we will be using Idris 2, a general purpose functional language with an expressive type system combining dependent types to enforce complex invariants and linear logic to track resource usage. We will demonstrate how a simple library can capture ideas from concurrent separation logic by providing proof-carrying concurrent primitives. These make it impossible to write into memory one does not own or to release a lock without having proven that its associated invariant has been re-established. They also guarantee that whatever is read from the shared memory is invariant-respecting. This will culminate in worked out example e.g. the definition of map-reduce primitives repeatedly and safely breaking down a buffer into chunks that can be processed concurrently.

Abstract

Hide Abstract

This talk summarizes recent work aiming at developing real-valued logics appropriate for reasoning about algebraic structures on metric spaces and as support for metatheoretical reasoning for approximated mathematical (exact) phenomena. The main application is generalizing the theory of Quantitative Algebras and Quantitative Equational Logics, but they also open the perspective of developing mathematical theories where identity is not the main metalogical predicate.

Abstract

Hide Abstract

Neuro-symbolic code simply refers to any (standard, symbolic) program in which some exact calculations are replaced by approximations given by neural networks or similar machine-learning algorithms. The purpose of proof-carrying neuro-symbolic code as a research direction is to propose languages or programming environments where implementation of such a system, as well as all necessary proofs of its safety, can be carried out in a sound and consistent way. This has proven to be a (programming language) challenge. However, some battles have been won. This talk will explain the existing challenges and the future directions.