title: Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic

authors:
Qiyuan Zhao
George Pîrlea
Zhendong Ang
Umang Mathur
Ilya Sergey

abstract:
Array-based encodings of tree structures are often preferable to linked or abstract data type-based representations for efficiency reasons. Compared to the more traditional encodings, array-based trees do not immediately offer convenient induction principles, and the programs that manipulate them often implement traversals non-recursively, requiring complex loop invariants for their correctness proofs.

In this work, we provide a set of definitions, lemmas, and reasoning principles that streamline proofs about array-based trees and programs that work with them. We showcase our proof techniques via a series of small but characteristic examples, culminating with a large case study: verification of a C implementation of a recently published tree clock data structure in a Separation Logic embedded into Coq.


venue: cpp

title: Lean Formalization of Extended Regular Expression Matching with Lookarounds

authors:
Ekaterina Zhuchko
Margus Veanes
Gabriel Ebner

abstract: We present a formalization of a matching algorithm for extended regular expression matching based on locations and symbolic derivatives which supports intersection, complement and lookarounds and whose implementation mirrors an extension of the recent .NET NonBacktracking regular expression engine. The formalization of the algorithm and its semantics uses the Lean 4 proof assistant. The proof of its correctness is with respect to standard matching semantics.


title: Formalization of Differential Privacy in Isabelle/HOL

authors:
Tetsuya Sato
Yasuhiko Minamide

abstract: Differential privacy is a statistical definition of privacy that has attracted the interest of both academia and industry. Its formulations are easy to understand, but the differential privacy of databases is complicated to determine. One of the reasons for this is that small changes in database programs can break their differential privacy. Therefore, formal verification of differential privacy has been studied for over a decade. In this paper, we propose an Isabelle/HOL library for formalizing differential privacy in a general setting. To our knowledge, it is the first formalization of differential privacy that supports continuous probability distributions. First, we formalize the standard definition of differential privacy and its basic properties. Second, we formalize the Laplace mechanism and its differential privacy. Finally, we formalize the differential privacy of the report noisy max mechanism.


title: An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting

authors:
Dohan Kim
Teppei Saito
René Thiemann
Akihisa Yamada

abstract: In this paper, we present an Isabelle/HOL formalization of co-rewrite pairs for non-reachability analysis in term rewriting. In particular, we formalize polynomial interpretations over negative integers as well as the weighted path order (WPO) and its variant co-WPO. With this formalization, the verified certifier CeTA is now able to check such non-reachability proofs, including those for non-reachability problems of a database where existing tools fail to provide certified proofs.


title: Intrinsically Correct Sorting in Cubical Agda

authors:
Cass Alexandru
Vikraman Choudhury
Jurriaan Rot
Niels van der Weide

abstract: The paper "Sorting with Bialgebras and Distributive Laws" by Hinze et al. uses the framework of bialgebraic semantics to define sorting algorithms. From distributive laws between functors they construct pairs of sorting algorithms using both folds and unfolds. Pairs of sorting algorithms arising this way include insertion/selection sort and quick/tree sort. We extend this work to define intrinsically correct variants in cubical Agda. Our key idea is to index our data types by multisets, which concisely captures that a sorting algorithm terminates with an ordered permutation of its input list. By lifting bialgebraic semantics to the indexed setting, we obtain the correctness of sorting algorithms purely from the distributive law.


title: Leakage-Free Probabilistic Jasmin Programs

authors:
José Bacelar Almeida
Denis Firsov
Tiago Oliveira
Dominique Unruh

abstract: This paper presents a semantic characterization of leakage-freeness through timing side-channels for Jasmin programs. Our characterization covers probabilistic Jasmin programs that are not constant-time. In addition, we provide a characterization in terms of probabilistic relational Hoare logic and prove the equivalence between both definitions. We also prove that our new characterizations are compositional and relate our new definitions to existing ones from prior work, which could only be applied to deterministic programs. To provide practical evidence, we use the Jasmin framework to develop a rejection sampling algorithm and provide an EasyCrypt proof that ensures the algorithm's implementation is leakage-free while not being constant-time.


title: Certifying Rings of Integers in Number Fields

authors:
Anne Baanen
Alain Chavarri Villarello
Sander R. Dahmen

abstract: Number fields and their rings of integers, which generalize the rational numbers and the integers, are foundational objects in number theory. There are several computer algebra systems and databases concerned with the computational aspects of these. In particular, computing the ring of integers of a given number field is one of the main tasks of computational algebraic number theory. In this paper, we describe a formalization in Lean 4 for certifying such computations. In order to accomplish this, we developed several data types amenable to computation. Moreover, many other underlying mathematical concepts and results had to be formalized, most of which are also of independent interest. These include resultants and discriminants, as well as methods for proving irreducibility of univariate polynomials over finite fields and over the rational numbers. To illustrate the feasibility of our strategy, we formally verified entries from the Number fields section of the L-functions and modular forms database (LMFDB). These concern, for several number fields, the explicitly given integral basis of the ring of integers and the discriminant. To accomplish this, we wrote SageMath code that computes the corresponding certificates and outputs a Lean proof of the statement to be verified.


title: Monadic Interpreters for Concurrent Memory Models: Executable Semantics of a Concurrent Subset of LLVM IR

authors:
Nicolas Chappe
Ludovic Henrio
Yannick Zakowski

abstract: Monadic interpreters have gained attention as a powerful tool for modeling and reasoning about first order languages. In particular in the Coq ecosystem, the Choice Tree (CTree) library provides generic tools to craft such interpreters in presence of divergence, stateful effects, failure, and non-determinism. This monadic approach allows the definition of semantics for programming languages that are modular in its effects, compositional w.r.t. its syntax, and executable. This paper demonstrates the use of CTrees to formalize a semantics for concurrency and weak memory models. We instantiate the approach over a minimal concurrent subset of LLVM IR. Our semantics is built in successive stages, interpreting each aspect of the semantics separately. In particular, a stage encodes multi-threading as an interleaving semantics, and another implements a weak memory model that supports various LLVM memory orderings. Furthermore, the modularity of the approach makes it possible to plug a different source language or memory model by changing a single interpretation phase. By leveraging the notions of (bi)similarity on CTrees, we establish the equational theory of our constructions, show how to transport equivalences through our layered construction, and prove simulation results between memory models. Finally, our model is executable, hence the semantics can be tested by extraction to OCaml.


title: Verified and Efficient Matching of Regular Expressions with Lookaround

authors:
Agnishom Chattopadhyay
Angela W. Li
Konstantinos Mamouras

abstract: Regular expressions can be extended with lookarounds for contextual matching. This paper discusses a Coq formalization of the theory of regular expressions with lookarounds. We provide an efficient and purely functional algorithm for matching expressions with lookarounds and verify its correctness. The algorithm runs in time linear in both the size of the regular expression as well as the input string. Our experimental results provide empirical support to our complexity analysis. To the best of our knowledge, this is the first formalization of a linear-time matching algorithm for regular expressions with lookarounds.


title: Formalized Burrows-Wheeler Transform

authors:
Louis Cheung
Alistair Moffat
Christine Rizkallah

abstract: The Burrows-Wheeler transform (BWT) is an invertible lossless transformation that permutes input sequences into alternate sequences of the same length that frequently contain long localized regions that involve clusters consisting of just a few distinct symbols, and sometimes also include long runs of same-symbol repetitions. As a consequence, the BWT is used in a wide range of tools, from everyday file compression software, such as bzip2, to highly sophisticated bioinformatics tools, such as DNA sequencers, where an efficient encoding of genomic sequences is essential. As such, ensuring the correctness of the BWT is critical. In this paper, we present the first formal verification of both the BWT and its inverse. Our verification efforts are conducted in Isabelle/HOL. Building on a recent formalization of the suffix array construction algorithm, we provide a mechanized proof of correctness, invertibility, and termination for both transformations. By doing so, we address the gap in the formal verification of compression algorithms, ensuring that the BWT can be safely deployed in critical applications such as genomic data analysis. This work thereby also provides the necessary foundation for verifying the various algorithms for compression and text search that operate on BWT-transformed sequences.


title: An Isabelle/HOL Framework for Synthetic Completeness Proofs

abstract: Proof assistants like Isabelle/HOL provide the perfect opportunity to develop more than just one-off formalizations, but frameworks for developing new results within a given area. Completeness results for logical calculi often include bespoke versions of Lindenbaum's lemma. In this paper, I mechanize an abstract, transfinite version of the lemma and use it to build witnessed, maximal consistent sets (MCSs) for any notion of consistency that satisfies a few requirements. I prove abstract results about when MCSs reflect the proof rules of the underlying calculi. Finally, I formalize a process for mechanically calculating saturated set conditions from a given logic's semantics. This separates the truth lemma that connects MCS-membership and satisfiability into semantic and syntactic components, giving concrete proof obligations for each operator of the logic. To illustrate the framework's applicability, I instantiate it with propositional, first-order, modal and hybrid logic examples. I mechanize strong completeness for each logic, even for uncountably large languages, proving that, if a formula is valid under a set of assumptions, then we can derive it from a finite subset.


title: Formalizing the One-Way to Hiding Theorem

authors:
Katharina Heidler
Dominique Unruh

abstract: As the standardization process for post-quantum cryptography progresses, the need for computer-verified security proofs against classical and quantum attackers increases. Even though some tools are already tackling this issue, none are foundational. We take a first step in this direction and present a complete formalization of the One-way to Hiding (O2H) Theorem, a central theorem for security proofs against quantum attackers. With this new formalization, we build more secure foundations for proof-checking tools in the quantum setting. Using the theorem prover Isabelle, we verify the semi-classical O2H Theorem by Ambainis, Hamburg and Unruh (Crypto 2019) in different variations. We also give a novel (and for the formalization simpler) proof to the O2H Theorem for mixed states and extend the theorem to non-terminating adversaries. This work provides a theoretical and foundational background for several verification tools and for security proofs in the quantum setting.


title: Machine Checked Proofs and Programs in Algebraic Combinatorics

abstract: We present a library of formalized results around symmetric functions and the character theory of symmetric groups. Written in Coq/Rocq and based on the Mathematical Components library, it covers a large part of the contents of a graduate level textbook in the field. The flagship result is a proof of the Littlewood-Richardson rule, which computes the structure constants of the algebra of symmetric function in the schur basis which are integer numbers appearing in various fields of mathematics, and which has a long history of wrong proofs. A specific feature of algebraic combinatorics is the constant interplay between algorithms and algebraic constructions: algorithms are not only in computations, but also are key ingredients in definitions and proofs. As such, the proof of the Littlewood-Richardson rule deeply relies on the understanding of the execution of the Robinson-Schensted algorithm. Many results in this library are effective and actually used in computer algebra systems, and we discuss their certified implementation.


title: CRIS: The Power of Imagination in Specification and Verification (Invited Talk)

abstract: Just as imaginary numbers extend real numbers and simplify certain mathematical proofs, we introduce the concept of imaginary specifications to enhance program verification. In mathematics, imaginary numbers enable expressing intermediate steps that cannot be captured using real numbers alone, offering natural proof decomposition that reduces complex proofs into simpler, more manageable steps. Similarly, our work introduces imaginary specifications in program verification through CRIS (Contextual Refinement with Imaginary Specification), our novel verification tool. CRIS with imaginary specifications provides a unified framework to inherently marry two fundamental approaches to program verification: separation logic with pre/post conditions as specifications, and program refinement with abstract programs as specifications. This unification not only enables proof simplification via proof decomposition but also enables elegant expression of hard-to-express properties, such as separation logic conditions involving IO events and logical atomicity---properties that traditionally require intricate mechanisms or are difficult to specify.


title: Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems

authors:
Christina Kirk
Aart Middeldorp

abstract: We report on the formalization of a sufficient condition for confluence of first-order left-linear rewrite systems within the proof assistant Isabelle/HOL. This criterion, originally proposed by Okui (1998), is based on simultaneous critical pairs, which finitely represent peaks consisting of a multi-step and a normal step. It properly subsumes the formalized result on development-closed critical pairs.


title: Tactic Script Optimisation for Aesop

abstract: White-box proof search tactics such as Coq's auto, Isabelle's auto and Lean's Aesop apply proof rules that often translate directly to lower-level tactics. When these search tactics find a proof, they can, at least in principle, generate a tactic script, i.e. a sequence of lower-level tactics that proves the goal. Such a script can then replace the typically much slower invocation of the search tactic, or it can be used to understand and debug the search. However, at least for Aesop, naively generated scripts are highly unidiomatic. For example, they use tactics that users would typically avoid; they apply these tactics in an unusual order; and they do not use Lean's constructs for structuring tactic scripts. To address these issues, I propose a three-stage optimisation pipeline that transforms naive scripts into scripts resembling a human-written Lean proof. The first stage replaces less idiomatic tactics with more idiomatic ones, checking that the two sequences of tactics produce the same result. The second stage permutes the tactics in the script to bring them into a natural, depth-first order, which then allows us to use Lean's structuring constructs. The third stage runs some straightforward post-processing passes.


title: CertiCoq-Wasm: A Verified WebAssembly Backend for CertiCoq

authors:
Wolfgang Meier
Martin Jensen
Jean Pichon-Pharabod
Bas Spitters

abstract: We contribute CertiCoq-Wasm, a verified WebAssembly backend for CertiCoq. CertiCoq-Wasm is implemented and verified in the Coq proof assistant, and is mechanised with respect to the WasmCert-Coq formalisation of the WebAssembly standard. CertiCoq-Wasm works from CertiCoq's minimal lambda calculus in administrative normal form (ANF), and produces WebAssembly programs with reasonable performance. It implements Coq's primitive integer operations as efficient WebAssembly instructions, identifying a corner case in their implementation that led to unsoundness. We compare CertiCoq-Wasm against other, partially verified extraction mechanisms from Coq to WebAssembly, benchmarking running time and program size. We demonstrate the practical usability of CertiCoq-Wasm with two case studies: we extract and run a Gallina program on the web, and a ConCert smart contract on the Concordium blockchain.


title: Further Tackling Post Correspondence Problem and Proof Generation

authors:
Akihiro Omori
Yasuhiko Minamide

abstract: Post Correspondence Problem (PCP) is a classic example of an undecidable problem, with various heuristic algorithms proposed to tackle its instances. In this study, we focus on solving a particular subset of instances known as PCP[3,4]. We introduce a novel algorithm that leverages regular lan- guages and automata theory to identify inductive invariants within the transition systems associated with these instances, enabling us to demonstrate the unsolvability of instances. Additionally, we manually found some inductive invariants using an interactive tool developed specifically for this pur- pose. As a result, we successfully solved all instances except for two. To ensure the correctness of our results, we gen- erated proofs for each instance that can be verified using Isabelle/HOL.


title: Formally Verified Hardening of C Programs against Hardware Fault Injection

authors:
Basile Pesin
Sylvain Boulmé
David Monniaux
Marie-Laure Potet

abstract: A fault attack is a malicious manipulation of the hardware (e.g., electromagnetic or laser pulse) that modifies the behavior of the software. Fault attacks typically target sensitive applications such as cryptography services, authentication, boot-loaders or firmware updaters. They can be defended against by adding countermeasures, that is, control flow checks and redundancies, either in the hardware, or in the software running on it. In particular, software countermeasures may be added automatically during compilation. In this paper, we describe a formally verified implementation of this approach in the CompCert verified compiler for the C language. We implemented two existing countermeasures protecting the control flow of the program as program transformations over a middle-end intermediate representation of CompCert, RTL. We proved that these countermeasures are correct, that is, they do not change the observable behavior of the program during an execution without fault injection. We then modeled the effect of a fault on the behavior of the program as an extension of the semantic model of RTL. We used this new model to formally prove the efficacy of the countermeasure: all attacks are either caught, or produce no observable effects. In addition to this formal reasoning, we evaluated the protected program using Lazart, a tool for symbolic fault injection, and measured the effect of optimizations on security and performance.


title: Prospects for Computer Formalization of Infinite-Dimensional Category Theory (Invited Talk)

abstract: As mathematics becomes increasingly complicated, the prospect of using a computer proof assistant to (i) certify the correctness of one’s own work and (ii) interact with the formalized mathematical literature becomes increasingly attractive. In this talk, we will describe some challenges that arise when it comes to formalizing weak infinite-dimensional category theory, specifically the theory of ∞-categories developed by Joyal and Lurie. We introduce two parallel ongoing collaborative efforts to formalize ∞-category theory in two different proof assistants: Lean and Rzk. We show some sample formalized proofs to highlight the advantages and drawbacks of each formal system and explain how you could contribute to this effort. This involves joint work with Mario Carneiro, Dominic Verity, Nikolai Kudasov, and Jonathan Weinberger.


title: Nominal Matching Logic with Fixpoints

authors:
Mircea Sebe
Maribel Fernández
James Cheney

abstract: Matching logic is the foundation of the K semantic environment for the specification of programming languages and automated generation of evaluators and verification tools. NLML is a formalization of nominal logic, which facilitates specification and reasoning about languages with binders, as a matching logic theory. Many properties of interest are inductive, and to prove them an induction principle modulo alpha-equality is required. In this paper we show that an alpha-structural Induction Principle for any nominal binding signature can be derived in an extension of NLML with set variables and fixpoint operators. We illustrate the use of the principle to prove properties of the λ-calculus, the computation model underlying functional programming languages. The techniques generalize to other languages with binders. The proofs have been written in and generated using Metamath Zero.


title: The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic

authors:
Simon Friis Vindum
Aïna Linn Georges
Lars Birkedal

abstract: As separation logic is a logic of resources, the way in which resources can soundly change and be updated is a fundamental aspect. Such changes have typically been restricted to certain local or frame-preserving updates. However, recently we have seen separation logics where the restriction to frame-preserving updates seems to be a hindrance towards achieving the ideal program reasoning rules. In this, paper we propose a novel nextgen modality that enables reasoning across generations where each generational change can update resources in ways that are non-local and non-frame-preserving. We implement the idea as an extension to the Iris base logic, which enriches Iris with an entirely new capability: the ability to make non-frame-preserving updates to ghost state. We show that two existing Iris modalities are special cases of the nextgen modality. Our “extension” can thus also be seen as a generalization and simplification of the Iris base logic. To demonstrate the utility of the nextgen modality we use it to construct a separation logic for a programming language with explicit stack allocation and with a return operation that clears entire stack frames. The nextgen modality is used to great effect in the reasoning rule for return, where a modular and practical reasoning rule is otherwise out of reach. This is the first separation logic for a high-level programming language with stack allocation. We sketch ideas for future work in other domains where we think the nextgen modality can be useful.


title: Split Decisions: Explicit Contexts for Substructural Languages

authors:
Daniel Zackon
Chuta Sano
Alberto Momigliano
Brigitte Pientka

abstract: A central challenge in mechanizing the meta-theory of substructural languages is modeling contexts. Although various ad hoc approaches to this problem exist, we lack a set of good practices and a simple infrastructure that can be leveraged for mechanizing a wide range of substructural systems. In this work, we describe Contexts as Resource Vectors (CARVe), a general syntactic infrastructure for managing substructural contexts, where elements are annotated with tags from a resource algebra denoting their availability. Assumptions persist as contexts are manipulated since we model resource consumption by changing their tags. We may thus define relations between substructural contexts via simultaneous substitutions without the need to split them. Moreover, we establish a series of algebraic properties about context operations that are typically required to carry out proofs in practice. CARVe is implemented in the proof assistant Beluga. To illustrate best practices for using our infrastructure, we give a detailed reformulation of the linear sequent calculus and bidirectional linear λ-calculus in terms of CARVe’s context operations and prove their equivalence using the aforementioned algebraic properties. In addition, we apply CARVe to mechanize a diverse set of systems, from the affine λ-calculus to the session-typed process calculus CP, giving us confidence that CARVe is sufficiently general to mechanize a broad range of substructural systems.


title: A CHERI C Memory Model for Verified Temporal Safety

authors:
Vadim Zaliva
Kayvan Memarian
Brian Campbell
Ricardo Almeida
Nathaniel Wesley Filardo
Ian Stark
Peter Sewell

abstract: Memory safety concerns continue to be a major source of security vulnerabilities. The CHERI architecture, as instantiated in prototype CHERI-RISC-V cores, the Arm Morello system, and Microsoft's CHERIoT embedded core, provides fine-grained memory access control through unforgeable hardware capabilities. The impact of CHERI on spatial memory safety is well understood. This paper systematically examines temporal memory safety within CHERI C -- a dialect of the C programming language for CHERI -- and proposes a formal approach to defining and ensuring it. In particular: 1) we examine the impact of five existing capability revocation mechanisms on CHERI C semantics and present a specialised object memory model tailored to CHERI C; 2) we introduce a new CHERI-specific pointer provenance tracking scheme; and 3) we formally define the security guarantees provided by this memory model, supported by a Coq proof of their correctness, expressed as invariants of the memory state.


title: Can We Formalise Type Theory Intrinsically without Any Compromise? A Case Study in Cubical Agda

authors:
Liang-Ting Chen
Fredrik Nordvall Forsberg
Tzu-Chun Tsai

abstract: We present an intrinsic representation of type theory in the proof assistant Cubical Agda, inspired by Awodey’s natural models of type theory. The initial natural model is defined as quotient inductive-inductive-recursive types, leading us to a syntax accepted by Cubical Agda without using any transports, postulates, or custom rewrite rules. We formalise some meta-properties such as the standard model, normalisation by evaluation for typed terms, and strictification constructions. Since our formalisation is carried out using Cubical Agda's native support for quotient inductive types, all our constructions compute at a reasonable speed. When we try to develop more sophisticated metatheory, however, the 'transport hell' problem reappears. Ultimately, it remains a considerable struggle to develop the metatheory of type theory using an intrinsic representation that lacks strict equations. The effort required is about the same whether or not the notion of natural model is used.


title: Building Blocks for Step-Indexed Program Logics

authors:
Thomas Somers
Jonas Kastberg Hinrichsen
Lennard Gäher
Robbert Krebbers

abstract:
Step-indexing and the later modality ▷ P are widely used in program logics. A key challenge in proofs in step-indexed logics is turning ▷ P into P, coined the later elimination problem. Later elimination cannot be done unconditionally, and has traditionally been linked one-to-one to the physical steps the program performs in the operational semantics. This one-to-one correspondence proved limiting in practice, and various techniques (flexible step-indexing and later credits) have been proposed to relax this correspondence.

Unfortunately, there exist many variations of these techniques with different features and proof rules. Moreover, integrating these techniques into a program logic for a specific domain (e.g., crash safety or trace refinement) requires non-trivial proof engineering of the metatheory. Our goal is to consolidate this situation. We introduce the physical-step modality—a modular building block that enables designers of program logics to obtain all existing features and rules with little proof engineering effort. We integrate our modality into various projects in the Iris ecosystem (Actris, RefinedRust, Perennial, Trillium), and show that it unlocks new proof rules that these projects previously did not support. All our results are mechanized in the Rocq prover.


title: Adhesive Category Theory for Graph Rewriting in Rocq

authors:
Samuel Arsac
Russ Harmer
Damien Pous

abstract:
We design a Rocq library about adhesive categories, using Hierarchy Builder (HB). It is built around two hierarchies. The first is for categories, with usual categories at the bottom and adhesive categories at the top, with weaker variants of adhesive categories in between. The second is for morphisms (notably isomorphisms, monomorphisms and regular monomorphisms). Each level of these hierarchies is equipped with several interfaces to define instances.

We cover basic categorical concepts such as pullbacks and equalizers, as well as results specific to adhesive categories. Using this library, we formalize two central theorems of categorical graph rewriting theory: the Church-Rosser theorem and the concurrency theorem. We provide several instances, including the category of types, the category of finite types, the category of simple graphs and categories of presheaves. We detail the implementation choices we made and report on the usage of HB for this formalization work.


title: Towards Composable Proofs of Cache Coherence Protocols

authors:
Martina Camaioni
Yann Herklotz
Tz-Ching Yu
Thomas Bourgeat

abstract:
Verifying cache coherence protocols is a notoriously difficult problem. At the intersection between distributed protocol and computer architecture, it has long served as a premier target for formal methods. Current verification approaches hinge on the challenging discovery of large global inductive invariants. This paper introduces an alternative proof strategy that tames the complexity through two main contributions: protocol decomposition and a framework of local invariants.

We prove the correctness of the standard MSI protocol compositionally by independently verifying the simpler MI and SI subprotocols and proving MSI behaves as their combination. This decomposition revealed a useful insight: the invariants necessary in these proofs can be established using a small set of simple local invariants: invariants between a single cache and the parent and memory, eliminating complex global reasoning across children caches. We demonstrate how our approach reduces the number of required invariants from several dozens to hundreds in prior work to a small, structured and manageable set, simplifying the proof of correctness. The entire development is formalized in Lean 4.


title: Formalizing Polynomial Laws and the Universal Divided Power Algebra

authors:
Antoine Chambert-Loir
María Inés de Frutos-Fernández

abstract:
The goal of this paper is to present an ongoing formalization, in the framework provided by the Lean/Mathlib mathematical library, of the construction by Roby (1965) of the universal divided power algebra. This is an analogue, in the theory of divided powers, of the classical algebra of polynomials. It is a crucial tool in the development of crystalline cohomology; it is also used in p-adic Hodge theory to define the crystalline period ring. As an algebra, this universal divided power algebra has a fairly simple definition that shows that it is a graded algebra. The main difficulty in Roby’s theorem lies in constructing a divided power structure on its augmentation ideal. To that aim, Roby identified the graded pieces with another universal structure: homogeneous polynomial laws.

We formalize the first steps of the theory of polynomial laws and show how future work will allow to complete the formalization of the above-mentioned divided power structure. We report on various difficulties that appeared in this formalization: taking care of universes, extending to semirings some aspects of the Mathlib library, and coping with several instances of ”invisible mathematics”.


title: Certifying the Decidability of the Word Problem in Monoids at Large

authors:
Reinis Cirpons
Florent Hivert
Assia Mahboubi
Guillaume Melquiond
James D. Mitchell
Finn Smith

abstract: While the word problem for monoids is undecidable in general, having a decision procedure for some finitely presented monoid of interest has numerous applications. This paper presents a toolbox for the Rocq proof assistant that can be used to verify the decidability of the word problem for a given monoid and, in some cases, to produce the corresponding decision procedure. As this verification can be computationally intensive, the toolbox heavily relies on proofs by reflection guided by an external oracle. This approach has been successfully used on several large presentations from the literature, as well as on a database of one million 1-relation monoids. The huge size of this database forced some unusual considerations onto the Rocq formalization, so that the formal proofs could be checked in a reasonable amount of time.


title: A Recipe for Modular Verification of Generic Tree Traversals

authors:
Laila Elbeheiry
Michael Sammler
Robbert Krebbers
Derek Dreyer
Deepak Garg

abstract:
Data structures based on trees and tree traversals are ubiquitous in computer systems. Many low-level programs, including some implementations of critical systems like page tables and the web browser DOM, rely on generic tree-traversal functions that traverse tree nodes in a pre-determined order, applying a client-provided operation to each visited node. Developing a general approach to specifying and verifying such traversals is tricky since the client-provided per-node operation can be stateful and may potentially depend on or modify the structure of the tree being traversed.

In this paper, we present a recipe for (semi-)automated verification of such generic, stateful tree traversals. Our recipe is (a) general: it applies to a range of tree traversals, in particular, pre-, post- and in-order depth-first traversals; (b) modular: parts of a traversal’s proof can be reused in verifying other similar traversals; (c) expressive: using the specification of a tree traversal, we can verify clients that use the traversal in a variety of different ways; and (d) automatable: many proof obligations can be discharged automatically.

At the heart of our recipe is a novel use of tree zippers to represent a logical abstraction of the tree traversal state, and zipper transitions as an abstraction of traversal steps. We realize our recipe in the RefinedC framework in Rocq, which allows us to verify a number of different tree traversals and their clients written in C.


title: Using Ghost Ownership to Verify Union-Find and Persistent Arrays in Rust

authors:
Arnaud Golfouse
Armaël Guéneau
Jacques-Henri Jourdan

abstract:
The type system of Rust enforces the “shared xor mutable” principle, which forbids mutation of shared memory. This principle eases verification in Rust, but certain programs require circumventing it with the mechanism of interior mutability. Thus, supporting interior mutability in a deductive verification tool is difficult. The Verus tool demonstrated the use of ghost resources to that end. So far, this mechanism has only been applied to Verus in order to verify primarily system code.

We extend the deductive verification tool Creusot with support for linear ghost resources. We show how Creusot’s full support for mutable borrows enables better specifications for primitives of linear ghost code. We apply this methodology to the verification of two data structures using sharing and mutation: union-find and persistent arrays.


title: Higher Order Differential Calculus in Mathlib

abstract: We report on the higher-order differential calculus library developed inside the Lean mathematical library Mathlib. To support a broad range of applications, we depart in several ways from standard textbook definitions: we allow arbitrary fields of scalars, we work with functions defined on domains rather than full spaces, and we integrate analytic functions in the broader scale of smooth functions. These generalizations introduce significant challenges, which we address from both the mathematical and the formalization perspectives.


title: Precise Reasoning about Container-Internal Pointers with Logical Pinning

authors:
Yawen Guan
Clément Pit-Claudel

abstract:
Most separation logics hide container-internal pointers for modularity. This makes it difficult to specify container APIs that temporarily expose those pointers to the outside, and to verify programs that use these APIs.

We present logical pinning, a lightweight borrowing model for sequential programs that allows users to selectively track container-internal pointers at the logical level. Our model generalizes the magic-wand operator for representing partial data structures, making it easy to write and prove precise specifications, including pointer-stability properties. Because it only changes the way representation predicates and specifications are written, our approach is compatible with most separation logic variants.

We demonstrate the practicality of logical pinning by verifying small but representative pointer-manipulating programs, and deriving more precise versions of common container specifications. In doing so, we show that our approach subsumes some well-known proof patterns, simplifies some complex proofs, and enables reasoning about program patterns not supported by traditional specifications. All of our results are mechanized in the Rocq proof assistant, using the CFML library.


title: A Lambda-Superposition Tactic for Isabelle/HOL

abstract: This paper introduces slam, an Isabelle/HOL tactic and automated theorem prover based on the λ-superposition calculus. An alternative to Isabelle’s metis tactic, slam targets higher-order logic directly, avoiding the overhead introduced by metis’s translations to first-order logic. Like metis, slam can be used as a Sledgehammer backend to reconstruct proofs produced by external higher-order automated theorem provers such as E, Vampire, and Zipperposition.


title: Layers of Confluence for Actors

authors:
Ludovic Henrio
Einar Broch Johnsen
Åsmund Aqissiaq Arild Kløvstad
Violet Ka I Pun
Yannick Zakowski

abstract: This paper introduces a novel proof technique to show that parallel or distributed programs exhibit confluent behaviour, even when the execution of these programs is inherently non-deterministic. The proposed method allows us to prove the confluence of programs for which standard properties such as strong confluence or commutativity of operations do not hold. Our technique builds on a method to prove the confluence of rewrite systems by de Bruijn, which we first adapt and formalise in Rocq. This method can be seen as a specialised induction principle for proving confluence. The paper further considers how this induction principle can be used in the context of programming languages. We show how the proof method can be instantiated to establish confluence conditions for programs in a small Actor-like programming language and demonstrate the application of the method to prove the confluence of a class of programs that cannot be proven to have deterministic behaviour by standard techniques.


title: Certified Symbolic Finite Transducers: Formalization and Applications to String Analysis

authors:
Shuanglong Kan
Anthony W. Lin

abstract: Finite Transducers (FTs) extend the capabilities of Finite Au- tomata (FAs) by enabling the transformation of input strings into output strings. In many practical applications — includ- ing program analysis, string constraint solving, and analysis of security-critical sanitizers — Symbolic FTs (SFTs) and Sym- bolic FAs (SFAs) are used instead of the explicitly represented models. To circumvent to the notorious state-space explosion problem caused by an extremely large alphabet size (e.g. Unicode), SFTs and SFAs allow the representation of the alphabet as an effective boolean algebra including finite unions of intervals, as well as SMT-Algebras. The security-critical nature of many of these applications demands trustworthy implementations of such systems. To this end, we present the first formalization of SFTs and their most important algorithms in Isabelle/HOL. To evaluate the effectiveness of our formalization, we apply the formalized SFTs to two applications: (1) sanitizers for web applications used for preventing XSS attacks, and (2) string solving, which increasingly employs intricate string replacement operations. Our experimental results demonstrate that our methods are competitive with the existing unverified implementations.


title: A Rose Tree Is Blooming (Proof Pearl)

abstract:
Game trees are a fundamental mathematical abstraction for analyzing games, often implemented as rose trees in functional programming. We can construct rose trees by starting from an initial state and iteratively applying the function that provides the states one move away, an approach known as an anamorphism (or colloquially, an unfold).

In ML or Haskell, finite and infinite rose trees share the same type, but proof assistants typically distinguish them: finite trees as inductive, infinite ones as coinductive. With the inductive approach, defining the unfold function is tricky but we obtain a finite tree that is easy to compute with and easy to reason about. With the coinductive approach, defining the unfold function is easy but we obtain a potentially infinite tree, which is harder to reason about since we must resort to proof techniques like bisimulation. In this paper, we compare the inductive and coinductive approaches to game trees, implement unfold functions for both, and prove the soundness and completeness of both unfold functions (with respect to the game) in the Rocq Prover. We illustrate these techniques with implementations of a tic-tac-toe game and a simple SAT solver.


title: Bar Inductive Predicates for Constructive Algebra in Rocq

abstract: In constructive commutative algebra, we revive the bar inductive characterization of Noetherian rings. We contribute the first constructive (axiom free) implementation of Hilbert's basis theorem, in the Rocq proof assistant. We show that the polynomial ring R[X] is Noetherian when the ring R is Noetherian, without assuming any additional condition on R, like coherence or else strong discreteness. We also contribute and implement a new result, that Noetherian rings are closed under direct products, again without assuming any supplementary condition on rings. We study induction principles for Noetherian rings, and relate bar Noetherianity with some other constructive characterizations.


title: Brack: A Verified Compiler for Scheme via CakeML

authors:
Pascal Y. Lasnier
Jeremy Yallop
Magnus O. Myreen

abstract: This paper describes Brack, which is a new verified compiler for Scheme. Brack compiles a substantial subset of Scheme, including first-class continuations, recursive bindings, first-class functions, mutable local variables, and lists, to CakeML, from where programs can be compiled to machine code. Compilation from Scheme to CakeML is based around a continuation-passing-style (CPS) transformation that naturally arises from Scheme’s small-step semantics. We have formally established the correctness of Brack in the HOL4 theorem prover.


title: Mechanized Dominator Tree Certification

abstract: In modern compilers, many optimizations and analyses, in particular those based on the SSA form, rely on dominance information, so computing dominators efficiently is an important problem. The classic algorithm to compute dominators in a control flow graph is the one designed by Lengauer and Tarjan in 1979. Other efficient algorithms have been proposed since. Previous works formally verified less efficient algorithms, and formally validated parts of the Lengauer-Tarjan algorithm, but there is no complete formal verification or validation of any of the fast algorithms computing dominators so far. In 2016, Georgiadis and Tarjan described a method to tackle these. They defined a certificate with which it becomes easy to validate dominators. Following their method, we successfully implemented and proved correct a validator of dominators in the Rocq Prover, inside the CompCertSSA verified compiler. This is the first complete mechanized certification of a fast algorithm computing dominators.


title: Mechanizing Synthetic Tait Computability in Istari

authors:
Runming Li
Yue Yao
Robert Harper

abstract: Categorical gluing is a powerful technique for proving meta-theorems of type theories such as canonicity and normalization. Synthetic Tait Computability (STC) provides an abstract treatment of the complex gluing models by internalizing the gluing category into a modal dependent type theory with a phase distinction. This work presents a mechanization of STC in the Istari proof assistant. Istari is a Martin-L'of-style extensional type theory with equality reflection, which avoids much of the explicit transport reasoning typically found in intensional proof assistants. This work develops a reusable library for synthetic phase distinction, including modalities, extension types, and strict glue types, and applies it to two case studies: (1) a canonicity model for dependent type theory with dependent products and booleans with large elimination, and (2) a Kripke canonicity model for the cost-aware logical framework. Our results demonstrate that the core STC constructions can be formalized essentially verbatim in Istari, preserving the elegance of the on-paper arguments while ensuring machine-checked correctness.


title: Modular Specifications and Implementations of Random Samplers in Higher-Order Separation Logic

authors:
Virgil Marionneau
Félix Sassus Bourda
Alejandro Aguirre
Lars Birkedal

abstract:
Probabilistic programs have a myriad of applications, from randomized algorithms to statistical modeling, and as such have inspired a long tradition of probabilistic program logics to verify their correctness. One essential use of probabilistic programs is to program new samplers from more primitive samplers, e.g., to generate samples from more complex distributions only given a primitive uniform sampler. Such samplers are an ideal case study for probabilistic program logics, to ensure that they implement the target distributions correctly. But proving correctness is often not enough, one also wants to reason about clients of these samplers, which require their specifications to be expressive and reusable.

In this work, we propose a methodology for giving specifications to samplers that are detailed enough to prove that they are correct, and expressive enough to reason about their clients. We propose our methodology for Eris, a recent probabilistic program logic based on the Iris separation logic. We identify what makes the proof rules and reasoning principles for primitive distributions in Eris work, and we distill them into a distribution typeclass. This presents at an abstract level the requirements that a concrete implementation of a target distribution should satisfy, and provides reasoning principles for clients of the interface. Working at this level of abstraction allows us to prove correctness results, as well as to derive additional reasoning principles for all implementations that adhere to the typeclass interface. We instantiate this approach to a variety of samplers for classical distributions, such as binomials, geometrics and beta-binomials.


title: Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions

authors:
Tomaz Mascarenhas
Harun Khan
Abdalrhman Mohamed
Andrew Reynolds
Haniel Barbosa
Clark W. Barrett
Cesare Tinelli

abstract: Determining the satisfiability of formulas involving nonlinear real arithmetic and transcendental functions is necessary in many applications, such as formally verifying dynamic systems. Doing this automatically generally requires costly and intricate methods, which limits their applicability. In the context of SMT solving, Incremental Linearization was introduced recently to facilitate reasoning on this domain, via an incomplete but easy to implement and highly effective approach. The approach, based on abstraction-refinement via an incremental axiomatization of the nonlinear and transcendental operators, is currently implemented in the SMT solvers MathSAT and cvc5. The cvc5 implementation is also proof-producing. This paper presents two contributions: a formalization in the Lean proof assistant of the proof calculus employed by cvc5, and an extension of the lean-smt plugin to reconstruct the proofs produced by cvc5 using this proof calculus. These contributions ensure the soundness of the proof calculus, making the underlying algorithm more trustworthy. Moreover, they allow users to check cvc5 results obtained via incremental linearization, as well as improve Lean’s automation for problems in nonlinear arithmetic. We discuss how we modeled the rules in the proof assistant and the challenges encountered while formalizing them, as well as the issues in reconstructing proofs involving these rules in Lean, and how we solved them.


title: A Certifying Proof Assistant for Synthetic Mathematics in Lean

authors:
Wojciech Nawrocki
Joseph Hua
Mario Carneiro
Yiming Xu
Spencer Woolfson
Shuge Rong
Sina Hazratpour
Steve Awodey

abstract: Synthetic theories such as homotopy type theory axiomatize classical mathematical objects such as spaces up to homotopy. Although theorems in synthetic theories translate to theorems about the axiomatized structures on paper, this fact has not yet been exploited in proof assistants. This makes it challenging to formalize results in classical mathematics using synthetic methods. For example, Cubical Agda supports reasoning about cubical types, but cubical proofs have not been translated to proofs about cubical set models, let alone their topological realizations. To bridge this gap, we present SynthLean: a proof assistant that combines reasoning using synthetic theories with reasoning about their models. SynthLean embeds Martin-Löf type theory as a domain-specific language in Lean, supporting a bidirectional workflow: constructions can be made internally in Martin-Löf type theory as well as externally in a model of the theory. A certifying normalization-by-evaluation typechecker automatically proves that internal definitions have sound interpretations in any model; conversely, semantic entities can be axiomatized in the syntax. Our implementation handles universes, Σ, Π, and identity types, as well as arbitrary axiomatized constants. To provide a familiar experience for Lean users, we reuse Lean’s tactic language and syntax in the internal mode, and base our formalization of natural model semantics on Mathlib. By taking a generic approach, SynthLean can be used to mechanize various interpretations of internal languages such as the groupoid, cubical, or simplicial models of homotopy type theory in HoTTLean.


title: Verified VCG and Verified Compiler for Dafny

authors:
Daniel Nezamabadi
Magnus O. Myreen
Yong Kiam Tan

abstract: Dafny is a verification-aware programming language that comes with a compiler and static program verifier. However, neither the compiler nor the verifier is proved correct; in fact, soundness bugs have been found in both tools. This paper shows that the aforementioned Dafny tools can be developed with foundational correctness guarantees. We present a functional big-step semantics for an imperative subset of Dafny and, based on this semantics, a verified verification condition generator (VCG) and a verified compiler for Dafny. The subset of Dafny we have formalized includes mutually recursive method calls, while loops, and arrays---these language features are significant enough to cover challenging examples such as McCarthy's 91 function and array-based programs that are used when teaching Dafny. The verified VCG allows one to prove functional correctness of annotated Dafny programs, while the verified compiler can be used to compile verified Dafny programs to CakeML programs. From there, one can obtain executable machine code via the (already verified) CakeML compiler, all while provably maintaining the functional correctness guarantees that were proved for the source-level Dafny programs. Our work has been mechanized in the HOL4 theorem prover.


title: Computing Solutions for Systems of Multivariate Ordinary Differential Equations in Rocq

abstract: We formalize a solver for initial value problems for systems of multivariate analytic ordinary differential equations in the sense of constructive/computable analysis, using the Rocq proof assistant. The construction follows the classical proof of the Cauchy-Kovalevskaya theorem, computing the Taylor series expansion of the solution by iteratively deriving its coefficients. We prove that the computed Taylor series converges and provide explicit bounds on the truncation error, ensuring the error can be made arbitrarily small. Instead of relying on a concrete implementation of constructive reals, we develop an abstract framework using type classes and setoids, allowing the formalization to remain flexible and compatible with different implementations. Additionally, we extend the formalization to a more efficient variant based on interval arithmetic and illustrate its practical use with several examples.


title: Foundational Verification of Running-Time Bounds for Interactive Programs

authors:
Andy Tockman
Pratap Singh
Andres Erbsen
Samuel Gruetter
Adam Chlipala

abstract: Some important domains of software demand concrete bounds on how long functions may run, for instance for real-time cyberphysical systems where missed deadlines may damage industrial machinery. Such programs may interact with external devices throughout execution, where time deadlines ought to depend on, for instance, sensor readings (e.g. we only scramble to close a valve immediately when a sensor reports that a tank is about to overflow). We present the first software-development toolchain that delivers first-principles proofs of meaningful time bounds for interactive machine code, while allowing all per-application programming and verification to happen at the source-code level. We allow C-like programs to be proved against separation-logic specifications that also constrain their running time, and such proofs are composed with verification of a compiler to RISC-V machine code. All components are implemented and proved inside the Rocq proof assistant, producing final theorems whose statements depend only on machine-language formal semantics and some elementary specification constructions for describing running time. As a capstone case study, we extended a past verification (of a real microcontroller-based cyberphysical system) to bound time between arrival of network packets and actuation of an attached device.


title: Adding Sorts to an Isabelle Formalization of Superposition

authors:
Balázs Tóth
Martin Desharnais-Schäfer
Jasmin Blanchette

abstract: The superposition calculus has been formalized in Isabelle/HOL twice before but in both cases without a type system. Nowadays, modern superposition provers support types. We extend an existing Isabelle formalization of untyped superposition with simple monomorphic types, or sorts. This extension is straightforward on paper but surprisingly tricky to implement formally. We also use this opportunity to refactor the proof text to avoid quadruplicated definitions, lemmas, and proofs about terms, atoms, literals, and clauses. The extended formalization and its refactoring benefit from Isabelle's locales, structured Isar proofs, and Sledgehammer proof tool.


title: Enhancing Symbolic Execution with Machine-Checked Safety Proofs

authors:
David Trabish
Shachar Itzhaky

abstract: Symbolic execution (SE) is a program analysis technique that executes the program with symbolic inputs. In modern SE engines, when the analysis of a given program is exhaustive, the analyzed program is typically considered safe, i.e., free of bugs, but no formal guarantees are provided to support this. Rather than aiming for a formally verified SE engine that will provide such guarantees, which is challenging, we propose a systematic approach where each individual analysis additionally generates a formal safety proof that validates the symbolic computations that were carried out. Our approach consists of two main components: A formal framework connecting concrete and symbolic semantics, and an instrumentation of the SE engine which generates formal safety proofs based on this framework. We showcase our approach by implementing a KLEE-based prototype that operates on a subset of LLVM IR with integers and generates proofs in Rocq. Our preliminary experiments show that our approach generates proofs that have reasonable validation times, while the instrumentation incurs only a minor overhead on the SE engine. In addition, during the implementation of our prototype, we found previously unknown semantic implementation issues in KLEE.


title: Cylindrical Algebraic Decomposition in Coq/Rocq

abstract: The Cylindrical Algebraic Decomposition (CAD in short) is a fundamental tool of semi-algebraic geometry. It is a doubly-exponential time algorithm that enables most famously to eliminate quantifiers from a formula in the theory of real closed fields. In particular, it allows to decide the satisfiability of problems involving sets of comparisons between polynomials. The present article describes the first formalization of a correctness proof of this algorithm in a proof assistant.


venue: dls

title: Language constructs for context-oriented programming: an overview of ContextL

authors:
Pascal Costanza
Robert Hirschfeld

abstract: ContextL is an extension to the Common Lisp Object System that allows for Context-oriented Programming. It provides means to associate partial class and method definitions with layers and to activate and deactivate such layers in the control flow of a running program. When a layer is activated, the partial definitions become part of the program until this layer is deactivated. This has the effect that the behavior of a program can be modified according to the context of its use without the need to mention such context dependencies in the affected base program. We illustrate these ideas by providing different UI views on the same object while, at the same time, keeping the conceptual simplicity of object-oriented programming that objects know by themselves how to behave, in our case how to display themselves. These seemingly contradictory goals can be achieved by separating class definitions into distinct layers instead of factoring out the display code into different classes.


title: Flexible object encapsulation for ambient-oriented programming

authors:
Wolfgang De Meuter
Éric Tanter
Stijn Mostinckx
Tom Van Cutsem
Jessie Dedecker

abstract: In the emerging field of Ambient Intelligence (AmI), software is deployed in wireless open networks of mobile devices. Such open networks require stringent security measures as unknown and untrusted hosts may join the network. In an object-oriented language, where objects are distributed and moved across the network, it thus becomes important to be able to enforce object encapsulation. In contemporary object-oriented programming languages, powerful operations such as object extension (inheritance), cloning and reflection, are typically provided via omnipotent language operators that fail to uphold object encapsulation, because they can be applied without the explicit consent of the concerned object. This paper formulates a language design principle --extreme encapsulation-- that precludes the use of such harmful operators, and proposes a corresponding language feature --method attributes-- that makes it possible to provide the flexibility of object extension, cloning and reflection without compromising on object encapsulation. Although some existing object-based languages can be said to support extreme encapsulation, our contribution is to support it in a delegation-based, prototype-based language named ChitChat.


title: Dynamic data polyvariance using source-tagged classes

authors:
Steven Alexander Spoon
Olin Shivers

abstract: The DDP (Demand-driven/Pruning) analysis algorithm allows us to perform data-flow analyses of programming languages that are dynamically typed and have higher-order control flow, such as Smalltalk or Scheme. Because it is demand-driven and employs search pruning, it scales to large code bases. However, versions of the algorithm previously described [19] do not handle data polymorphism well, conservatively merging separate data flows that go through distinct instantiations of a collection type. In this paper, we describe a new extension to DDP that helps to disentangle these flows, permitting more precise results. The extension is based on source-tagging classes so that each reference to a class in the source code yields a subdivision of the type associated with that class. An initial implementation of this polyvariant analysis has been added to the DDP-based tool Chuck, a part of the integrated Squeak program-development environment; we show examples of the tool in action.


title: Compile-time meta-programming in a dynamically typed OO language

abstract: Compile-time meta-programming allows programs to be constructed by the user at compile-time. Although LISP derived languages have long had such facilities, few modern languages are capable of compile-time meta-programming, and of those that do many of the most powerful are statically typed functional languages. In this paper I present the dynamically typed object orientated language Converge which allows compile-time meta-programming in the spirit of Template Haskell. Converge demonstrates that integrating powerful, safe compile-time meta-programming features into a dynamic language requires few restrictions to the flexible development style facilitated by the paradigm. In this paper I detail Converge's compile-time meta-programming facilities, much of which is adapted from Template Haskell, contain several features new to the paradigm. Finally I explain how such a facility might be integrated into similar languages.


title: Higher order messaging

authors:
Marcel Weiher
Stéphane Ducasse

abstract: We introduce Higher Order Messaging, a higher order programming mechanism for dynamic object-oriented languages. Higher Order Messages allow user-defined message dispatch mechanism to be expressed using an optimally compact syntax that is a natural extension of plain messaging and also have a simple conceptual model. They can be implemented without extending the base language and operate through language bridges.


title: RPython: a step towards reconciling dynamically and statically typed OO languages

authors:
Davide Ancona
Massimo Ancona
Antonio Cuni
Nicholas D. Matsakis

abstract: Although the C-based interpreter of Python is reasonably fast, implementations on the CLI or the JVM platforms offers some advantages in terms of robustness and interoperability. Unfortunately, because the CLI and JVM are primarily designed to execute statically typed, object-oriented languages, most dynamic language implementations cannot use the native bytecodes for common operations like method calls and exception handling; as a result, they are not able to take full advantage of the power offered by the CLI and JVM.


title: Highly dynamic behaviour adaptability through prototypes with subjective multimethods

authors:
Sebastián González
Kim Mens
Patrick Heymans

abstract: With the advent of ambient intelligence and advances in mobile hardware technology, the next generation of software systems will require the ability to gracefully and dynamically adapt to changes in their surrounding environment. Contemporary languages provide no dedicated support to this end, thus requiring software developers to achieve this run-time adaptability through the use of specific design patterns and architectural solutions. As a consequence, all possible variability points of mobile systems need to be anticipated up front. Instead, we aim at solving the problem at the language level. We propose a new programming language called Ambience that provides dedicated language mechanisms to manage changing contexts and deal with run-time adaptation of mobile applications to those contexts. The language abstractions we propose are based on a prototype-based programming model that features multimethods and subjective object behaviour. We illustrate and motivate our approach by means of two running examples that were implemented in our language.


title: Dynamic ownership in a dynamic language

authors:
Donald Gordon
James Noble

abstract: Object aliasing causes as many problems in dynamic languages as it does in static languages. Most existing work on aliasing, such as ownership types, relies on static checking based on annotations and type declarations. We introduce ConstraintedJava, a scripting language based on BeanShell that provides dynamic ownership checking. Dynamic ownership provides the encapsulation benefits of static ownership types but preserves the flexibility of dynamic languages.


title: Relationally-parametric polymorphic contracts

authors:
Arjun Guha
Jacob Matthews
Robert Bruce Findler
Shriram Krishnamurthi

abstract: The analogy between types and contracts raises the question of how many features of static type systems can be expressed as dynamic contracts. An important feature missing in prior work on contracts is parametricity, as represented by the polymorphic types in languages like Standard ML.


title: Bringing dynamic languages to .NET with the DLR

abstract: From the beginning, Microsoft's .NET framework was designed to support a broad range of different programming languages on a Common Language Runtime (CLR). The CLR provides shared services to these languages ranging from a world-class GC and JIT to a sandboxed security model to tools integration for debugging and profiling. Sharing these features has two huge benefits for languages on the CLR. First, it's easier to implement a language because lots of difficult engineering work is already done for you. Second, and more importantly, these languages can seamlessly work together and share libraries and frameworks so that each language can build on the work of the others. The CLR has good support for dynamic languages today. IronPython-1.0 demonstrates this. The new Dynamic Language Runtime (DLR) adds a small set of key features to the CLR to make it dramatically better. It adds to the platform a set of services designed explicitly for the needs of dynamic languages. These include a shared dynamic type system, standard hosting model and support to make it easy to generate fast dynamic code. With these additional features it becomes dramatically easier to build high-quality dynamic language implementations on .NET. More importantly, these features enable all of the dynamic languages which use the DLR to freely share code with other dynamic languages as well as with the existing powerful static languages on the platform such as VB.NET and C#.


title: Arrays of objects

abstract: This paper discusses key design decisions faced by a language design team while adding Object Oriented language features to Dyalog, a modern dialect of APL. Although classes and interfaces are first-class language elements in the new language, and arrays can both contain and be contained by objects, arrays are not objects. The use of object oriented features is optional, and users can elect to remain entirely in the functional and array paradigms of traditional APL. The choice of arrays as a "higher" level of organization allows APL's elegant notation for array manipulation to extend smoothly to arrays of objects.


title: Tradeoffs in retrofitting security: an experience report

abstract: In 1973, John Reynold's and James Morris' Gedanken language retrofit object-capability security into an Algol-like base. Today, there are active projects retrofitting Java, Javascript, Python, Mozart/Oz, OCaml, Perl, and Pict. These represent a variety of approaches, with different tradeoffs regarding legacy compatibility, safety, and expressivity. In this talk I propose a taxonomy of these approaches, and discuss some of the lessons learned to date.


title: Mirages: behavioral intercession in a mirror-based architecture

authors:
Stijn Mostinckx
Tom Van Cutsem
Stijn Timbermont
Éric Tanter

abstract: Mirror-based systems are object-oriented reflective architectures built around a set of design principles that lead to reflective APIs which foster a high degree of reusability, loose coupling with base-level objects and whose structure and design corresponds to the system being mirrored. However, support for behavioral intercession has been limited in contemporary mirror-based architectures, in spite of its many interesting applications. This is due to the fact that mirror-based architectures only support explicit reflection, while behavioral intercession requires implicit reflection. This work reconciles mirrors with behavioral intercession. We discuss the design of a mirror-based architecture with implicit mirrors that can be absorbed in the interpreter, and mirages, base objects whose semantics are defined by implicit mirrors. We describe and illustrate the integration of this reflective architecture for the distributed object-oriented programming language AmbientTalk.


title: Report on the probabilistic language scheme

abstract: Reasoning with probabilistic models is a widespread and successful technique in areas ranging from computer vision, to natural language processing, to bioinformatics. Currently, these reasoning systems are either coded from scratch in general-purpose languages or use formalisms such as Bayesian networks that have limited expressive power. In both cases, the resulting systems are difficult to modify, maintain, compose, and interoperate with. This work presents Probabilistic Scheme, an embedding of probabilistic computation into Scheme. This gives programmers an expressive language for implementing modular probabilistic models that integrate naturally with the rest of Scheme.


title: An adaptive package management system for scheme

authors:
Manuel Serrano
Erick Gallesio

abstract: This paper presents a package management system for the Scheme programming language. It is inspired by the Comprehensive Perl Archive Network (CPAN) and various GNU/Linux distributions. It downloads, installs, and prepares source codes for execution. It manages the dependencies between packages. The main characteristic of this system is its neutrality with respect to the various Scheme implementations. It is neutral with respect to the language extensions that each Scheme implementation proposes and with respect to the execution environment of these implementations. This allows the programmer to blend, within the same program, independent components which have been developed and tested within different Scheme implementations. ScmPkg is available at: http://hop.inria.fr/scmpkg.


title: OMeta: an object-oriented language for pattern matching

authors:
Alessandro Warth
Ian Piumarta

abstract: This paper introduces OMeta, a new object-oriented language for pattern matching. OMeta is based on a variant of Parsing Expression Grammars (PEGs) [5]---a recognition-based foundation for describing syntax---which we have extended to handle arbitrary kinds of data. We show that OMeta's general-purpose pattern matching provides a natural and convenient way for programmers to implement tokenizers, parsers, visitors, and tree transformers, all of which can be extended in interesting ways using familiar object-oriented mechanisms. This makes OMeta particularly well-suited as a medium for experimenting with new designs for programming languages and extensions to existing languages.


title: Dynamic AspectJ

authors:
Ali Assaf
Jacques Noyé

abstract: This paper considers the difficulties linked to the static scheduling strategy of AspectJ and shows how to overcome them by turning to a more dynamic strategy, making it possible to order, cancel, and deploy aspects at runtime. We show that this more dynamic strategy can be obtained by a minor update of the semantics of AspectJ introducing the notion of current aspect group, that is, the aspects scheduled for the current join point. We show how to reflect this change at the language level and present a prototype of the resulting AspectJ variant, Dynamic AspectJ. This prototype reuses AspectJ to perform a first step of static weaving, which we complement by a second step of dynamic weaving, implemented through a thin interpretation layer. This can be seen as an interesting example of reconciling interpreters and compilers, the dynamic and the static world.


title: Filtered dispatch

authors:
Pascal Costanza
Charlotte Herzeel
Jorge Vallejos
Theo D'Hondt

abstract: Predicate dispatching is a generalized form of dynamic dispatch, which has strong limitations when arbitrary predicates of the underlying base language are used. Unlike classes, which enforce subset relationships between their sets of instances, arbitrary predicates generally do not designate subsets of each other, so methods whose applicability is based on predicates cannot be ordered according to their specificity in the general case. This paper introduces a decidable but expressive alternative mechanism called filtered dispatch that adds a simple preprocessing step before the actual method dispatch is performed and thus enables the use of arbitrary predicates for selecting and applying methods.


title: The Clojure programming language

abstract: Customers and stakeholders have substantial investments in, and are comfortable with the performance, security and stability of, industry-standard platforms like the JVM and CLR. While Java and C# developers on those platforms may envy the succinctness, flexibility and productivity of dynamic languages, they have concerns about running on customer-approved infrastructure, access to their existing code base and libraries, and performance. In addition, they face ongoing problems dealing with concurrency using native threads and locking. Clojure is an effort in pragmatic dynamic language design in this context. It endeavors to be a general-purpose language suitable in those areas where Java is suitable. It reflects the reality that, for the concurrent programming future, pervasive, unmoderated mutation simply has to go. Clojure meets its goals by: embracing an industry-standard, open platform - the JVM; modernizing a venerable language - Lisp; fostering functional programming with immutable persistent data structures; and providing built-in concurrency support via software transactional memory and asynchronous agents. The result is robust, practical, and fast. This talk will focus on the motivations, mechanisms and experiences of the implementation of Clojure.


title: The Lively Kernel: just for fun, let's take JavaScript seriously

abstract: The Sun Labs Lively Kernel is a new approach to Web programming. It provides a complete platform for Web applications, including dynamic graphics, network access, and development tools, and requires nothing more than available web browsers. We call the system "lively" for three reasons. It comes live off a web page. There is no installation. The entire system is written in JavaScript, and it becomes active as soon as the page is loaded by a browser. It can change itself and create new content. The Lively Kernel includes a basic graphics editor that allows it to alter and create new graphical content, and also a simple IDE that allows it to alter and create new applications. It comes with a basic library of graphical and computational components, and these, as well as the kernel, can be altered and extended on the fly. It can save new artifacts, even clone itself, onto new web pages. The kernel includes WebDAV support for browsing and extending remote file systems, and thus has the ability to save its objects and "worlds" (applications) as new active Web pages. The Lively Kernel uses only existing Web standards. The implementation and user language is JavaScript, known by millions and supported in every browser. The graphics APIs are built upon SVG (Scalable Vector Graphics), also available in major browsers. The network protocols used are asynchronous HTTP and WebDAV. The speaker will demonstrate the Lively Kernel and discuss various aspects of JavaScript as a programming language.


title: Efficient floating-point number handling for dynamically typed scripting languages

abstract: Typical implementations of dynamically typed languages treat floating-point numbers, or flonums, in a "boxed" form, since those numbers don't fit in a natural machine word if a few bits in the word are reserved for type tags. The naïve implementations allocate every instance of flonums in the heap, thus incur large overhead on numerically intensive computations. Compile-time type inference could eliminate boxing of some flonums, but it would be costly for highly dynamic scripting languages, in which a compiler runs every time a script is executed.


title: A parsing machine for PEGs

authors:
Sérgio Medeiros
Roberto Ierusalimschy

abstract: Parsing Expression Grammar (PEG) is a recognition-based foundation for describing syntax that renewed interest in top-down parsing approaches. Generally, the implementation of PEGs is based on a recursive-descent parser, or uses a memoization algorithm. We present a new approach for implementing PEGs, based on a virtual parsing machine, which is more suitable for pattern matching. Each PEG has a corresponding program that is executed by the parsing machine, and new programs are dynamically created and composed. The virtual machine is embedded in a scripting language and used by a patternmatching tool. We give an operational semantics of PEGs used for pattern matching, then describe our parsing machine and its semantics. We show how to transform PEGs to parsing machine programs, and give a correctness proof of our transformation.


title: Gradual typing with unification-based inference

authors:
Jeremy G. Siek
Manish Vachharajani

abstract: Static and dynamic type systems have well-known strengths and weaknesses. Gradual typing provides the benefits of both in a single language by giving the programmer control over which portions of the program are statically checked based on the presence or absence of type annotations. This paper studies the combination of gradual typing and unification-based type inference with the goal of developing a system that helps programmers increase the amount of static checking in their program. The key question in combining gradual typing and type inference is how should the dynamic type of a gradual system interact with the type variables of a type inference system. This paper explores the design space and shows why three straightforward approaches fail to meet our design goals. This paper presents a new type system based on the idea that a solution for a type variable should be as informative as any type that constrains the variable. The paper also develops an efficient inference algorithm and proves it sound and complete with respect to the type system.


title: Contextual values

abstract: Context-oriented programming proposes to treat execution context explicitly and to provide means for context-dependent adaptation at runtime. There are many mechanisms that can be used to make either variable bindings or application code adapt dynamically, like dynamically-scoped variables, dynamic layer activation, and contextual dispatch. There are no means however, to make actual values be context-dependent. This means that side effects engendered by dynamically-activated adaptations are potentially global. We propose contextual values: values that actually depend on the context in which they are looked at and modified. We explore how contextual values can be provided, either as a simple library or directly into the language through different designs, for which we provide the operational semantics in the form of Scheme interpreters. Being able to scope side effects to certain contexts is a step forward for context-oriented programming, and can have interesting applications in other areas like security and dynamic software evolution.


title: Language design: back to the future?

abstract: Programming languages are the medium used to express our wishes to a computer. Unlike human languages, we can alter, destroy, and create them at will. Despite this, mainstream programming languages are surprisingly homogeneous with the differences between them often amounting to little more than surface syntax issues. New ideas rarely get a toe-hold in the marketplace and those that do have typically been used for decades by a sizeable minority (e.g. dynamic typing). In this talk the speaker will suggest reasons for the inherent conservativeness of programming languages, their designers, and their users. He will look back at some largely forgotten languages - some older than others - that introduced distinctive language features, and offer thoughts on their successes and failures. He will show how a series of seemingly outlandish ideas scavenged from such languages can be blended together to form part of a coherent modern language - one that also aims to try and inject a few new memes of its own into the languages pool.


title: Groovy package templates: supporting reuse and runtime adaption of class hierarchies

authors:
Eyvind W. Axelsen
Stein Krogdahl

abstract: We show how package templates, a modularization mechanism originally developed for statically typed languages like Java and C#, can be applied to and implemented in a dynamic language like Groovy, by using the language's capabilities for meta-programming. We then consider a set of examples and discuss dynamic PT from the viewpoints of code modularization and reuse, and dynamic adaption of classes at runtime.


title: Context-oriented software transactional memory in common lisp

authors:
Pascal Costanza
Charlotte Herzeel
Theo D'Hondt

abstract: Software transactional memory (STM) is a promising approach for coordinating concurrent threads, for which many implementation strategies are currently being researched. Although some first steps exist to ease experimenting with different strategies, this still remains a relatively complex and cumbersome task. The reason is that software transactions require STM-specific dynamic crosscutting adaptations, but this is not accounted for in current STM implementations. This paper presents CSTM, an STM framework based on Context-oriented Progamming, in which transactions are modelled as dynamically scoped layer activations. It enables expressing transactional variable accesses as user-defined crosscutting concerns, without requiring invasive changes in the rest of a program. This paper presents a proof-of-concept implementation based on ContextL for Common Lisp, along with example STM strategies and preliminary benchmarks, and introduces some of ContextL's unique features for context-dependent variable accesses.


title: The ruby intermediate language

authors:
Michael Furr
Jong-hoon (David) An
Jeffrey S. Foster
Michael Hicks

abstract: Ruby is a popular, dynamic scripting language that aims to "feel natural to programmers" and give users the "freedom to choose" among many different ways of doing the same thing. While this arguably makes programming in Ruby easier, it makes it hard to build analysis and transformation tools that operate on Ruby source code. In this paper, we present the Ruby Intermediate Language (RIL), a Ruby front-end and intermediate representation that addresses these. RIL includes an extensible GLR parser for Ruby, and an automatic translation into an easy-to-analyze intermediate form. This translation eliminates redundant language constructs, unravels the often subtle ordering among side effecting operations, and makes implicit interpreter operations explicit. We also describe several additional useful features of RIL, such as a dynamic instrumentation library for profiling source code and a dataflow analysis engine. We demonstrate the usefulness of RIL by presenting a static and dynamic analysis to eliminate null pointer errors in Ruby programs. We hope that RIL's features will enable others to more easily build analysis tools for Ruby, and that our design will inspire the of similar frameworks for other dynamic languages.


title: Directing JavaScript with arrows

authors:
Yit Phang Khoo
Michael Hicks
Jeffrey S. Foster
Vibha Sazawal

abstract: JavaScript programmers make extensive use of event-driven programming to help build responsive web applications. However, standard approaches to sequencing events are messy, and often lead to code that is difficult to understand and maintain. We have found that arrows, a generalization of monads, are an elegant solution to this problem. Arrows allow us to easily write asynchronous programs in small, modular units of code, and flexibly compose them in many different ways, while nicely abstracting the details of asynchronous program composition. In this paper, we present Arrowlets, a new JavaScript library that offers arrows to the everyday JavaScript programmer. We show how to use Arrowlets to construct a variety of state machines, including state machines that branch and loop. We also demonstrate how Arrowlets separate computation from composition with examples such as a drag-and-drop handler and a bubblesort animation.


title: Fast type reconstruction for dynamically typed programming languages

authors:
Frédéric Pluquet
Antoine Marot
Roel Wuyts

abstract: Type inference and type reconstruction derive static types for program elements that have no static type associated with them. They have a wide range of usage, such as helping to eliminate the burden of manually specifying types, verifying whether a program is type-safe, helping to produce more optimized code or helping to understand programs. While type inference and type reconstruction is an active field of research, most existing techniques are interested foremost in the precision of their approaches, at the expense of execution speed. As a result, existing approaches are not suited to give direct feedback in development environments, where interactivity dictates very fast approaches. This paper presents a type reconstruction algorithm for variables that is extremely fast (in the order of milliseconds) and reasonably precise (75 percent). The system is implemented as a byte-code evaluator in several Smalltalk environments, and its execution speed and precision are validated on a number of concrete case studies.


title: Language embedding and optimization in mython

abstract: Mython is an extensible variant of the Python programming language. Mython achieves extensibility by adding a quotation mechanism that accepts an additional parameter as well as the code being quoted. The additional quotation parameter takes the form of a Mython expression. Unlike other user code, Mython evaluates the quotation parameter at compile-time. The result of the compile-time expression is a function that is used to both parse the quoted code, and extend the compile-time environment. By explicitly passing the compilation environment to compile-time quotation functions, Mython's parameterized quotation allows users to inject code into the language compiler. Injected code can extend the language by modifying the compilation phases, which are visible to the compilation environment. The Mython language is realized by the MyFront compiler, a tool for translating Mython into Python byte-code modules. This paper introduces the Mython language, describes the implementation and usage of the MyFront tool, and shows how MyFront can be used to implement domain-specific optimizations using a little rewrite language.


title: Contracts for first-class modules

authors:
T. Stephen Strickland
Matthias Felleisen

abstract: Behavioral software contracts express properties concerning the flow of values across component (modules, classes, etc) interfaces. These properties are often beyond the reach of theorem provers and are therefore monitored at run-time. When the monitor discovers a contract violation, it raises an exception that simultaneously pinpoints the contract violator and explains the nature of the violation.


title: Beyond static and dynamic scope

abstract: Traditional treatment of scoping in programming languages considers two opposite semantics: static scoping, where the scope of a binding is a block of program text, and dynamic scoping, where a binding is in effect during the whole reduction of an expression to a value. Static scoping and dynamic scoping are however but two points in the design space of scoping mechanisms. As a result, most proposed language mechanisms that rely on some notion of scoping, such as variable bindings of course, but also more exotic ones like aspects and mixin layers, adopt either one or the other semantics. As it turns out, these two semantics are sometimes too extreme, and a mixture of both is needed. To achieve this, language designers and/or programmers have to resort to ad hoc solutions. We present a general scoping model that simply expresses static and dynamic scoping, and that goes further by allowing fine-grained exploration of the design space of scoping. The model, called scoping strategies, gives precise control over propagation and activation of language mechanisms. While we have already studied it for aspects, we hereby show that the model is not restricted to aspects, by treating in depth its application to the most standard kind of adaptation: variable bindings. We also briefly discuss its application to mixin layers, and program monitoring. We believe that research in programming language constructs can benefit from a more flexible notion of scoping that goes beyond the static/dynamic dichotomy.


title: Hosting an object heap on manycore hardware: an exploration

authors:
David M. Ungar
Sam S. Adams

abstract: In order to construct a test-bed for investigating new programming paradigms for future systems (i.e. those with at least a thousand cores), we are building a Smalltalk virtual machine that attempts to efficiently use a collection of 56-on-chip caches of 64KB each to host a multi-megabyte object heap. In addition to the cost of inter-core communication, two hardware characteristics influenced our design: the absence of hardware-provided cache-coherence, and the inability to move a single object from one core's cache to another's without changing its address. Our design relies on an object table, and the exploitation of a user-managed caching regime for read-mostly objects. At almost every stage of our process, we obtained measurements in order to guide the evolution of our system.The architecture and performance characteristics of a manycore platform confound old intuitions by deviating from both traditional multicore systems and from distributed systems. The implementor confronts a wide variety of design choices, such as when to share address space, when to share memory as opposed to sending a message, and how to eke out the most performance from a memory system that is far more tightly integrated than a distributed system yet far less centralized than in a several-core system. Our system is far from complete, let alone optimal, but our experiences have helped us develop new intuitions needed to rise to the manycore software challenge.


title: Of scripts and programs: tall tales, urban legends, and future prospects

abstract: Scripting languages are playing an increasing role in today's software landscape due to their support for rapid and exploratory development. They typically have lightweight syntax, weak data privacy, dynamic typing, powerful aggregate data types, and allow execution of the completed parts of incomplete programs. While many of their uses are web-centric, scripting languages also show up in non-traditional domains such as space exploration and administration of the pension benefits entire countries. Considering their importance to the practice of computing, it is surprising to see that, in academic circles, scripting is still often viewed as an undisciplined and unprincipled attempt at programming. In this talk, I will summarize work carried in collaboration with IBM Research on bridging the divide between scripting and programming. I will motivate our investigations with some success stories of scripting languages used in unusual places. Then I will dispel some misconceptions about the nature of scripts with preliminary results from a large corpus analysis of programs written in a popular scripting language. Finally, I will talk about the design of a new language, called Thorn, that aims to ease the journey from scripts to programs (and back).


title: Optimization of dynamic languages using hierarchical layering of virtual machines

authors:
Alexander Yermolovich
Christian Wimmer
Michael Franz

abstract: Creating an interpreter is a simple and fast way to implement a dynamic programming language. With this ease also come major drawbacks. Interpreters are significantly slower than compiled machine code because they have a high dispatch overhead and cannot perform optimizations. To overcome these limitations, interpreters are commonly combined with just-in-time compilers to improve the overall performance. However, this means that a just-in-time compiler has to be implemented for each language.


title: Controlling dynamic module composition through an extensible meta-level API

authors:
Eyvind W. Axelsen
Stein Krogdahl
Birger Møller-Pedersen

abstract: In addition to traditional object-oriented (OO) concepts such as inheritance and polymorphism, several modularization and composition mechanisms like e.g. traits, mixins and virtual classes have emerged. The Package Template mechanism is another attempt at providing a flexible mechanism for modularization, composition and adaption.


title: Efficient interpretation using quickening

abstract: Just-in-time compilers offer the biggest achievable payoff performance-wise, but their implementation is a non-trivial, time-consuming task affecting the interpreter's maintenance for years to come, too. Recent research addresses this issue by providing ways of leveraging existing just-in-time compilation infrastructures.Though there has been considerable research on improving the efficiency of just-in-time compilers, the area of optimizing interpreters has gotten less attention as if the implementation of a dynamic translation system was the ultima ratio for efficiently interpreting programming languages. We present optimization techniques for improving the efficiency of interpreters without requiring just-in-time compilation thereby maintaining the ease-of-implementation characteristic that brought many people to implementing an interpreter in the first place.


title: Proxies: design principles for robust object-oriented intercession APIs

authors:
Tom Van Cutsem
Mark S. Miller

abstract: Proxies are a powerful approach to implement meta-objects in object-oriented languages without having to resort to metacircular interpretation. We introduce such a meta-level API based on proxies for Javascript. We simultaneously introduce a set of design principles that characterize such APIs in general, and compare similar APIs of other languages in terms of these principles. We highlight how principled proxy-based APIs improve code robustness by avoiding interference between base and meta-level code that occur in more common reflective intercession mechanisms.


title: Alias analysis for optimization of dynamic languages

authors:
Michael Gorbovitski
Yanhong A. Liu
Scott D. Stoller
Tom Rothamel
K. Tuncay Tekle

abstract: Dynamic languages such as Python allow programs to be written more easily using high-level constructs such as comprehensions for queries and using generic code. Efficient execution of programs then requires powerful optimizations - incrementalization of expensive queries and specialization of generic code. Effective incrementalization and specialization of dynamic languages require precise and scalable alias analysis.


title: Factor: a dynamic stack-based programming language

authors:
Sviatoslav Pestov
Daniel Ehrenberg
Joe Groff

abstract: Factor is a new dynamic object-oriented programming language. It began as an embedded scripting language and evolved to a mature application development language. The language has a simple execution model and is based on the manipulation of data on a stack. An advanced metaprogramming system provides means for easily extending the language. Thus, Factor allows programmers to use the right features for their problem domain. The Factor implementation is self-hosting, featuring an interactive development environment and an optimizing compiler. In this paper, the language and its implementation are presented.


title: Contracts for first-class classes

abstract: First-class classes add expressive power to class-based object-oriented languages. Most importantly, programmers can abstract over common scenarios with first-class classes. When it comes to behavioral software contracts, however, first-class classes pose significant challenges. In this paper, we present the first contract system for a programming language with first-class classes. The design has been implemented for Racket, which supports first-class classes and which implements mixins and traits as syntactic sugar. We expect that our experience also applies to languages with native mixins and/or traits.


title: Experiences with an icon-like expression evaluation system

abstract: The design of the Icon programming language's expression evaluation system, which can perform limited backtracking, was unique amongst imperative programming languages when created. In this paper I explain and critique the original Icon design and show how a similar system can be integrated into a modern dynamically typed language. Finally I detail my experiences of this system and offer suggestions for the lessons to be learned from it.