SPLS Glasgow 1^st July 2022

Fitch-style modal lambda calculi enable programming with necessity modalities in a typed lambda calculus by extending the typing context with a delimiting operator that is denoted by a lock. The addition of locks simplifies the formulation of typing rules for calculi that incorporate different modal axioms, but each variant demands different, tedious and seemingly ad hoc syntactic lemmas to prove normalization. In this work, we develop normalization by evaluation (NbE) for Fitch-style calculi that incorporate the K, T and 4 axioms of modal logic by leveraging their possible-world semantics. The NbE approach exploits the commonalities of these calculi in the possible-world semantics and isolates their differences to a specific parameter that determines the modal fragment, thus enabling reuse of the evaluation machinery and many lemmas proved in the process. Finally, we showcase several consequences of normalization for proving meta-theoretic properties of Fitch-style calculi based on different interpretations of the necessity modality in programming languages, such as capability safety, noninterference and a form of binding-time correctness.

Paper and mechanization available here.

TypOS is an experimental language specific to the domain of implementing type checking, type synthesis and type-directed elaboration algorithms, presented as concurrent actors. We develop the idea "A rule is a server for its conclusion and a client for its premises." into a framework where the judgment forms are presented as interaction protocols and the rules for a given judgment are collectively presented as an actor serving the judgment's protocol. A running actor may spawn new actors of which it is the client, each with its own channel. The parameters to each judgement thus acquire not only a syntactic category, but also a mode as input or output. With this stromger sense of information flow, the language of formulae occurring in rules naturally splits into patterns which analyse things coming and expressions which synthesize things going. Expressions may contain substitutions to be done, but patterns may not, because substitutions are hard to undo. More generally, the TypOS design strategy is to prevent practices likely to result in failure of metatheoretical safety properties. We pay particular attention to term variable scope, for example ensuring that no actor can learn the name of a variable bound by another. TypOS also supports the speculation of unknowns, which become monotonically more defined as constraints are solved: we thus have the one kind of shared memory that makes sense in a distributed setting. Actors can thus block if they need information which is not yet available: ensuring that resuming actors operate on up-to-date information is the implementation challenge which precipitated the whole effort.

TypOS is joint work with Guillaume Allais, Malin Altenmueller, Georgi Nakov, Fredrik Nordvall Forsberg and Craig Roy. GitHub repository.

Dependently-typed programming languages are becoming increasingly popular in the functional programming community, allowing programmers to express properties of logic and proofs as part of their implementation. Dependent types permit the programmer to implement safe programs, by encoding safety properties as parts of the types themselves; these properties can be encoded by permitting the types to depend on values. However, programming dependently-typed systems is still very difficult for the average software developer, who may have had some prior training with functional languages, such as Haskell, but lacks the background and experience in logic and type systems to make appropriate use of the dependent types to build strong safe systems as a part of their day-to-day practice.

Refactoring aims to provide programmers with the ability to systemically restructure their code to better reflect its purpose, making it more amenable to change and maintainability, or simply to make it more understandable. The advantage of refactoring tool support is that it not only presents the programmer with a structured set of well-defined transformations, but it also alleviates the error-prone burden of manually making modifications across an entire project that might contain thousands of source code modules. To date, however, there are no refactoring tools for dependently-typed programming languages.

In this talk, we address this problem by discussing a number of new refactorings to be implemented for the dependently-typed programming language, Pi-Forall, developed by Weirich. We particularly focus on refactorings for extending and maintaining data types in Pi-Forall. We demonstrate our prototype refactorings over a simple lambda calculus example and discuss our preliminary refactoring tool, RePi.