Renamingless Capture-Avoiding Substitution for Definitional Interpreters

Substitution is a common and popular approach to implementing name binding in definitional interpreters. A common pitfall of implementing substitution functions is variable capture. The traditional approach to avoiding variable capture is to rename variables. However, traditional renaming makes for an inefficient interpretation strategy....

Deriving a Symbolic Executor for Definitional Interpreters Suitable for the Study of Heuristics

Recent years have seen a surge of interest for dynamic testing techniques, one of which is symbolic execution. It is the main point of interest of this research paper, in which we give an overview of a framework for symbolically executing definitional interpreters. We will also discuss techniques that we made use of in developing the symbolic...

Validating Type Checkers Using Property-Based Testing

Manually testing definitional interpreters and their type checkers is a tedious and error-prone process which can largely benefit from automation. This study evaluates the effectiveness of property-based testing on errors in type checkers. Metrics used include the ability to catch different types of errors as well as the ability to provide a...

Validating Definitional Interpreters Using Property-Based Testing

This paper presents an evaluation of different generation methods of input expressions to definitional interpreters. We compare three different ways of generating expressions of a specified algebraic data type. The approaches that we describe are QuickCheck, SmallCheck and a uniform generation technique, as laid out in their original papers....

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...

From definitional interpreter to symbolic executor

Symbolic execution is a technique for automatic software validation and verification. New symbolic executors regularly appear for both existing and new languages and such symbolic executors are generally manually (re)implemented each time we want to support a new language. We propose to automatically generate symbolic executors from language...

Scopes and frames improve meta-interpreter specialization

DynSem is a domain-specific language for concise specification of the dynamic semantics of programming languages, aimed at rapid experimentation and evolution of language designs. To maintain a short definition-to-execution cycle, DynSem specifications are meta-interpreted. Meta-interpretation introduces runtime overhead that is difficult to...

Testing Code Generators against Definitional Interpreters

Large companies suffer from the increasing complexity that exist in their software systems. Evolving their software becomes even harder if we consider that a change in one system can affect several other parts of their software architecture. Especially banks that need to be always complied with regulations, have to constantly make changes in...

Typesafe by Definition for Languages with Explicit Deallocation

A definitional interpreter is an interpreter which uses the semantics of its own host language to define those of its object language. Traditionally, a seperate type safety proof is used for such an interpreter. Using a "typesafe-by-construction" approach, where the typesafety is proven by expressing the type system of the object language in the...

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...

A scalable infrastructure for teaching concepts of programming languages in Scala with WebLab: An experience report

In this paper, we report on our experience in teaching a course on concepts of programming languages at TU Delft based on Krishnamurthi's PAPL book with the definitional interpreter approach using Scala as meta-language and using the WebLab learning management system. In particular, we discuss our experience with encoding of definitional...