Verifying Well-Typedness Preservation of Refactorings using Scope Graphs

The goal of automated refactoring is to reduce maintenance effort. To realize this, programmers need to be able to trust or manually check that refactorings actually preserve behavior. To allow programmers to focus on such checks, automated refactorings should preserve program well-typedness. However, historically automated refactorings in...

Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages

An intrinsically-typed definitional interpreter is a concise specification of dynamic semantics, that is executable and type safe by construction. Unfortunately, scaling intrinsically-typed definitional interpreters to more complicated object languages often results in definitions that are cluttered with manual proof work. For linearly-typed...

Knowing when to ask: Sound scheduling of name resolution in type checkers derived from declarative specifications

There is a large gap between the specification of type systems and the implementation of their type checkers, which impedes reasoning about the soundness of the type checker with respect to the specification. A vision to close this gap is to automatically obtain type checkers from declarative programming language specifications. This moves...

Intrinsically-Typed Definitional Interpreters for Imperative Languages

A definitional interpreter defines the semantics of an object language in terms of the (well-known) semantics of a host language, enabling understanding and validation of the semantics through execution. Combining a definitional interpreter with a separate type system requires a separate type safety proof. An alternative approach, at least for...

Scopes describe frames: A uniform model for memory layout in dynamic semantics

Semantic specifications do not make a systematic connection between the names and scopes in the static structure of a program and memory layout, and access during its execution. In this paper we introduce a systematic approach to the alignment of names in static semantics and memory in dynamic semantics, building on the scope graph framework...