Programming Languages
Proof by induction plays a critical role in formal verification and mathematics at large. However, its automation remains as one of the long-standing challenges in Computer Science. To address this problem, we developed sem_ind. Given…
Interprocedural analysis refers to gathering information about the entire program rather than for a single procedure only, as in intraprocedural analysis. Interprocedural analysis enables a more precise analysis; however, it is complicated…
Differential lambda-calculus was first introduced by Thomas Ehrhard and Laurent Regnier in 2003. Despite more than 15 years of history, little work has been done on a differential calculus with integration. In this paper, we shall propose a…
In many applications one wants to identify identical subtrees of a program syntax tree. This identification should ideally be robust to alpha-renaming of the program, but no existing technique has been shown to achieve this with good…
The Belief-Desire-Intention (BDI) architecture is a popular framework for rational agents; most verification approaches are based on reasoning about implementations of BDI programming languages. We investigate an alternative approach based…
Refinement types decorate types with assertions that enable automatic verification. Like assertions, refinements are limited to binders that are in scope, and hence, cannot express higher-order specifications. Ghost variables circumvent…
We present an approach for implementing a formally certified loop-invariant code motion optimization by composing an unrolling pass and a formally certified yet efficient global subexpression elimination.This approach is lightweight: each…
Capability machines such as CHERI provide memory capabilities that can be used by compilers to provide security benefits for compiled code (e.g., memory safety). The existing C to CHERI compiler, for example, achieves memory safety by…
Naming conventions are an important concern in large verification projects using proof assistants, such as Coq. In particular, lemma names are used by proof engineers to effectively understand and modify Coq code. However, providing…
We introduce a method for proving almost sure termination in the context of lambda calculus with continuous random sampling and explicit recursion, based on ranking supermartingales. This result is extended in three ways. Antitone ranking…
Information flow control type systems statically restrict the propagation of sensitive data to ensure end-to-end confidentiality. The property to be shown is noninterference, asserting that an attacker cannot infer any secrets from made…
Session types are becoming popular and have been integrated in several mainstream programming languages. Nevertheless, while many programming languages consider asynchronous fifo channel communication, the notion of subtyping used in…
We explore and formalize the task of synthesizing programs over noisy data, i.e., data that may contain corrupted input-output examples. By formalizing the concept of a Noise Source, an Input Source, and a prior distribution over programs,…
This document presents the syntax, classification rules, realizability semantics, and soundness theorem for Cedille, an extrinsic (i.e., Curry-style) type theory extending the Calculus of Constructions, and designed for deriving of…
We present a new synthesis algorithm to solve program synthesis over noisy datasets, i.e., data that may contain incorrect/corrupted input-output examples. Our algorithm uses an abstraction refinement based optimization process to…
Rust is an emerging programming language that aims to prevent memory-safety bugs. However, the current design of Rust also brings side effects which may increase the risk of memory-safety issues. In particular, it employs OBRM…
We implement extraction of Coq programs to functional languages based on MetaCoq's certified erasure. As part of this, we implement an optimisation pass removing unused arguments. We prove the pass correct wrt. a conventional call-by-value…
Proponents of the programming language Prolog share the opinion Prolog is more appropriate for transforming XML-documents as other well-established techniques and languages like XSLT. In order to clarify this position this work proposes a…
We review state-of-the-art formal methods applied to the emerging field of the verification of machine learning systems. Formal methods can provide rigorous correctness guarantees on hardware and software systems. Thanks to the availability…
The use of low- and no-code modeling tools is today an established way in practice to give non-programmers an opportunity to master their digital challenges independently, using the means of model-driven software development. However, the…