Reductionism is a viable strategy for designing and implementing practical programming languages, leading to solutions which are easier to extend, experiment with and formally analyze. We formally specify and implement an extensible programming language, based on a minimalistic first-order imperative core language plus strong abstraction mechanisms, reflection and self-modification features. The language can be extended to very high levels: by using Lisp-style macros and code-to-code transforms which automatically rewrite high-level expressions into core forms, we define closures and first-class continuations on top of the core. Non-self-modifying programs can be analyzed and formally reasoned upon, thanks to the language simple semantics. We formally develop a static analysis and prove a soundness property with respect to the dynamic semantics. We develop a parallel garbage collector suitable to multi-core machines to permit efficient execution of parallel programs.

翻译：归约主义是设计和实现实用编程语言的一种可行策略，能够产生更易于扩展、实验和形式化分析的解决方案。我们基于极简的一阶命令式核心语言，结合强抽象机制、反射与自修改特性，形式化地规范并实现了一种可扩展编程语言。该语言可扩展至极高水平：通过使用Lisp风格宏以及将高层表达式自动重写为核心形式的代码到代码转换技术，我们在核心之上定义了闭包和一等续延。得益于该语言的简单语义，非自修改程序可被分析并予以形式化推理。我们形式化地开发了一项静态分析，并证明了其相对于动态语义的可靠性性质。为支持并行程序的高效执行，我们还开发了一种适用于多核机器的并行垃圾回收器。