Rascal：从代数规范到元编程

BODHI：精确的操作系统内核规范推断

BODHI: Precise OS Kernel Specification Inference

提出一种领域知识提示方法BODHI，通过结构化C到Python翻译指南增强少样本提示，在OSV-Bench基准上将Pass@1从55.10%提升至96.73%，缩小了通用代码生成与形式规范合成之间的差距。

A Tool for Describing and Checking Natural Semantics Definitions of Programming Languages

Many universities have courses and projects revolving around compiler or interpreter implementation as part of their degree programmes in computer science. In such teaching activities, tool support can be highly beneficial. While there are already several tools for assisting with development of the front end of compilers, tool support tapers off towards the back end, or requires more background experience than is expected of undergraduate students. Structural operational semantics is a useful and mathematically simple formalism for specifying the behaviour of programs and a specification lends…

恢复Java语言规范的语法关系

Recovering Grammar Relationships for the Java Language Specification

语法趋同是一种有助于发现同一语言或不同语言版本中不同语法之间关系的方法。该方法的关键元素是这些关系的可操作的、基于转换的表示。给定用于收敛的输入语法，它们被变换直到它们在结构上相等。变换是由原始操作符组成的;这些操作符的属性和组成的链提供了对语法之间关系的定量和定性的洞察。我们描述了一种改进的方法，语法收敛，我们使用它在一个主要的研究，在那里我们恢复所有的语法之间的关系，发生在不同版本的Java语言规范（JLS）。这些关系被表示为语法转换链，这些语法转换链捕获JLS语法之间的所有偶然或有意的差异。这种方法是机械化的，并受到受到不对称的二元收敛步骤的语法对之间的名词性和结构性差异的驱动。我们提出了基本的操作套件语法转换的详细信息，我们说明了该套件的JLS语法转换的许多例子。我们还描述了提取工作，这是需要使JLS语法适合自动化处理。我们包含了大量关于JLS融合过程的元数据，以便工作变得可重复和透明。

Practical Idiomatic Considerations for Checkable Meta-Logic in Experimental Functional Programming

Implementing a complex concept as an executable model in a strongly typed, purely functional language hits a sweet spot between mere simulation and formal specification. For research and education it is often desirable to enrich the algorithmic code with meta-logical annotations, variously embodied as assertions, theorems or test cases. Checking frameworks use the inherent logical power of the functional paradigm to approximate theorem proving by heuristic testing. Here we propose several novel idioms to enhance the practical expressivity of checking, namely meta-language marking, nominal axio…

Refinement Kinds: Type-safe Programming with Practical Type-level Computation (Extended Version)

This work introduces the novel concept of kind refinement, which we develop in the context of an explicitly polymorphic ML-like language with type-level computation. Just as type refinements embed rich specifications by means of comprehension principles expressed by predicates over values in the type domain, kind refinements provide rich kind specifications by means of predicates over types in the kind domain. By leveraging our powerful refinement kind discipline, types in our language are not just used to statically classify program expressions and values, but also conveniently manipulated as…

Wasm SpecTec：工程化形式语言标准

Wasm SpecTec: Engineering a Formal Language Standard

Wasm SpecTec 通过领域特定语言自动生成并检查 WebAssembly 形式规范及相关产物，减轻规范编写负担，推动标准化流程自动化。

Using human-in-the-loop synthesis to author functional reactive programs

Programs that respond to asynchronous events are challenging to write; they are difficult to reason about and tricky to test and debug. Because these programs can have a huge space of possible input timings and interleaving, the programmer may easily miss corner cases. We propose applying synthesis to aid programmers in creating programs more easily and with a higher degree of confidence in their correctness. We have written an efficient encoding of functional reactive programming (FRP) semantics based on functional programming over lists lifted in Rosette. We demonstrate that this technique i…

逻辑框架下的高阶抽象推理

Reasoning with Higher-Order Abstract Syntax in a Logical Framework

基于具有更高类型量化的直觉或线性逻辑的逻辑框架已成功地用于对程序设计语言和推理系统领域中的许多重要判断给出高级、模块化和形式化的规范。给定这样的规范，考虑证明框架中指定系统的属性是很自然的：例如，给定函数式程序设计语言的求值规范，证明该语言是确定性的或求值保留类型。开发这种推理框架的一个挑战是高阶抽象语法（HOAS），一种优雅的和声明性的对象级抽象和替换处理，很难在涉及归纳的证明中处理。在本文中，我们提出了一个元逻辑，可用于推理使用HOAS编码的判断，这个元逻辑是一个简单的直觉主义逻辑，承认高阶量化简单类型的非线性项（HOAS的关键成分），以及归纳和定义的概念的扩展。我们通过考虑直觉和线性逻辑的编码，探讨了HOAS编码的形式元理论分析的困难，并正式推导出这些逻辑的重要子集的割的容许性。然后，我们提出了一种方法，以避免高阶抽象语法的好处和分析所产生的编码的能力之间的明显的权衡。我们通过涉及简单函数式和命令式程序设计语言PCF和PCF：=的示例来说明这种方法。我们正式推导出这样的属性，作为唯一性的类型，主题减少，确定性的评价，和等价的过渡语义和自然语义表示的评价。

A Formal Algebraic Framework for DSL Composition

We discuss a formal framework for using algebraic structures to model a meta-language that can write, compose, and provide interoperability between abstractions of DSLs. The purpose of this formal framework is to provide a verification of compositional properties of the meta-language. Throughout our paper we discuss the construction of this formal framework, as well its relation to our team's work on the DARPA V-SPELLS program via the pipeline we have developed for completing our verification tasking on V-SPELLS. We aim to give a broad overview of this verification pipeline in our paper. The p…

Formalization of Metatheory of the Quipper Quantum Programming Language in a Linear Logic

We develop a linear logical framework within the Hybrid system and use it to reason about the type system of a quantum lambda calculus. In particular, we consider a practical version of the calculus called Proto-Quipper, which contains the core of Quipper. Quipper is a new quantum programming language under active development and recently has gained much popularity among the quantum computing communities. Hybrid is a system that is designed to support the use of higher-order abstract syntax (HOAS) for representing and reasoning about formal systems implemented in the Coq Proof Assistant. In th…

ModelCC中抽象模型到具体模型映射的DSL

A DSL for Mapping Abstract Syntax Models to Concrete Syntax Models in ModelCC

ModelCC是一个基于模型的解析器生成器，它将语言设计与语言处理相结合。ModelCC提供了两种不同的机制来指定从抽象语法模型到具体语法模型的映射：在抽象语法模型规范之上定义的元数据注释和用于定义ASM-CSM映射的域特定语言。使用领域特定语言来指定从抽象语法模型到具体语法模型的映射允许为同一抽象语法模型定义多个具体语法模型。在本文中，我们描述了ModelCC域特定语言的抽象语法模型到具体的语法模型映射，我们展示了它的能力，提供了一个元定义的域特定语言。

函数式程序验证编译的高阶抽象方法

A Higher-Order Abstract Syntax Approach to the Verified Compilation of Functional Programs

我们认为，功能性程序设计语言的编译器的实现和验证大大简化了采用高阶表示的语法称为高阶抽象语法或HOAS。HOAS的基本思想是使用一种元语言，它为绑定相关概念提供内置的逻辑处理。通过将元语言嵌入到更大的编程或推理框架中，可以将对象语言中的绑定结构的处理吸收到系统的元理论中，从而大大简化整体实现和推理过程。我们在这篇论文中提出并证明了上述论点的有效性的方法来验证执行的编译器转换的函数程序，利用HOAS。在这种方法中，函数程序的转换首先以基于规则的关系规范的形式表达。这些规范被渲染成语言lambda Prolog的程序。一方面，这些程序直接作为实现。另一方面，它们可以用作Abella系统的输入，该系统允许我们证明关于它们的属性，从而证明关于实现的属性。lambda Prolog和Abella都支持使用HOAS方法。因此，它们构成了一个框架，可用于在验证编译中测试HOAS方法的好处。我们用它们来实现和验证一个编译器的代表性的功能程序设计语言，体现了许多编译器的核心，这些语言的转换。在这两个编程和推理阶段，我们展示了如何使用的HOAS方法显着简化了绑定结构的表示，操作，分析和推理。