Flag-Based Big-Step Semantics

Reasoning about Iteration and Recursion Uniformly based on Big-step Semantics

A reliable technique for deductive program verification should be proven sound with respect to the semantics of the programming language. For each different language, the construction of a separate soundness proof is often a laborious undertaking. In language-independent program verification, common aspects of computer programs are addressed to enable sound reasoning for all languages. In this work, we propose a solution for the sound reasoning about iteration and recursion based on the big-step operational semantics of any programming language. We give inductive proofs on the soundness and re…

A meta-theory for big-step semantics

It is well-known that big-step semantics is not able to distinguish stuck and non-terminating computations. This is a strong limitation as it makes very difficult to reason about properties involving infinite computations, such as type soundness, which cannot even be expressed. We show that this issue is only apparent: the distinction between stuck and diverging computations is implicit in any big-step semantics and it just needs to be uncovered. To achieve this goal, we develop a systematic study of big-step semantics: we introduce an abstract definition of what a big-step semantics is, we de…

Pretty-big-step-semantics-based Certified Abstract Interpretation（Preliminary version）

Pretty-big-step-semantics-based Certified Abstract Interpretation (Preliminary version)

我们提出了一种技术，用于从自然语义规范的程序设计语言的语义程序分析。该技术基于一种特殊的语义，称为pretty-big-step语义。我们提出了一个漂亮的大步骤语义的语言与简单的对象称为O 'While，并指定了一系列的仪表的语义，明确了流程的值在程序中。这导致了基于语义的依赖性分析，在核心，例如，污染分析在软件安全中的应用用Coq证明助手实现了形式化。

结合小步和大步语义来验证循环优化

Combining Small-Step and Big-Step Semantics to Verify Loop Optimizations

本文提出结合小步和大步语义的方法，用于验证循环优化，通过引入抽象行为语义实现结构变换与局部变换的统一，提升编译器验证的表达能力。

面向并发的共归纳大步语义

Coinductive Big-Step Semantics for Concurrency

在SOS 2010上发表的一篇论文中，我们开发了一个框架，用于交互式输入-输出的大步骤语义结合发散，基于共归纳和混合归纳共归纳概念，评价和终止敏感弱双相似性。与标准的归纳定义的大步骤语义相反，这个框架正确地处理分歧;特别是，产生一些可观察的效果，然后发散的运行，不会“丢失”。在这里，我们在一个简单的示例语言上扩展了这种共享变量并发的方法。我们以建构性逻辑发展我们语义的元理论。

不耗尽，不浪费：大步语义的资源感知可靠性

Don't exhaust, don't waste: Resource-aware soundness for big-step semantics

通过扩展lambda演算的语义和类型系统，实现资源使用追踪，确保良类型程序在计算中既不耗尽也不浪费资源，并采用余归纳技术证明资源感知可靠性。

具有交互式I/O的While的恢复、弱双相似性和大步语义：混合归纳-共归纳的练习

Resumptions, Weak Bisimilarity and Big-Step Semantics for While with Interactive I/O: An Exercise in Mixed Induction-Coinduction

我们通过构造性类型论的眼镜来看待具有交互式I/O的语言的操作语义。从我们早期的工作，基于共归纳跟踪的语义虽然，我们定义了几个大步骤的语义，而与交互式I/O，基于删除和终止敏感的弱双相似性。这需要在共归纳定义中嵌套归纳定义，这在数学上和在证明助手中实现的观点上都是有趣的。在第一次定义了一个基本的语义的声明中明确的内部动作（延迟）的delictions，我们引入了一个语义的无延迟delictions，基本上消除了有限的延迟序列的飞行从这些delictions是响应。最后，我们还研究了一个语义方面的无延迟的附加选项，一个沉默的分歧选项。这种语义取决于收敛和发散之间的决定，并且只等价于经典的基本语义。我们已经完全正式化了我们在Coq的发展。

While的基于共归纳迹的大步语义的霍尔逻辑

A Hoare logic for the coinductive trace-based big-step semantics of While

在寻找一个基本的框架，推理可观察到的行为的程序，可能不会终止，我们以前设计了一个基于跟踪的大步骤的语义虽然。在这种语义中，轨迹和评估（将程序运行的初始状态与它们产生的轨迹相关联）都是共归纳定义的。在终止运行时，这种语义与标准的基于归纳状态的语义一致。在这里，我们提出了一个霍尔逻辑对应我们的共归纳基于迹的语义，并证明它的声音和完整的。我们的逻辑包括标准的部分正确性状态为基础的霍尔逻辑以及总正确性的变化：他们是可嵌入的。在相反的方向上，投影可以被构造：在我们的基于迹的逻辑中的霍尔三元组的推导可以被转换为在基于状态的逻辑中的转换的、较弱的霍尔三元组的推导。由于我们使用的是建设性的底层逻辑，因此我们可以推理的程序属性范围具有良好的结构;特别是，我们可以区分终止性和非发散性，例如，无界经典全搜索不能终止，但仍然是无发散的。我们的元理论也是完全建设性的，我们已经在Coq中将其形式化了。

From Big-Step to Small-Step Semantics and Back with Interpreter Specialisation

We investigate representations of imperative programs as constrained Horn clauses. Starting from operational semantics transition rules, we proceed by writing interpreters as constrained Horn clause programs directly encoding the rules. We then specialise an interpreter with respect to a given source program to achieve a compilation of the source language to Horn clauses (an instance of the first Futamura projection). The process is described in detail for an interpreter for a subset of C, directly encoding the rules of big-step operational semantics for C. A similar translation based on small…

λ演算的概率操作语义

Probabilistic Operational Semantics for the Lambda Calculus

研究了纯λ演算的非确定性扩展的概率操作语义.在这种语义中，一个项计算为（有限或无限）值分布。小步和大步语义都是归纳和共归纳定义的。此外，小步和大步语义产生相同的结果，无论是在调用的值和调用的名称。Plotkin的CPS翻译进行了扩展，以适应选择操作符和正确的操作语义。最后，所得到的系统的表达能力进行了研究：微积分是健全的和完整的可计算的概率分布。

信号处理的操作语义

Operational semantics for signal handling

信号是Unix中进程间通信的一种轻量级形式。当进程接收到信号时，控制流被中断，并运行先前安装的信号处理程序。信号处理让人联想到异常处理和进程的并发交织。在本文中，我们研究了不同的方法来形式化信号处理的操作语义，并比较了一系列的例子。我们发现，大步骤风格的操作语义是非常适合建模信号处理。我们通过采用标准ML定义中定义的异常约定，将异常处理与信号处理的大步语义集成在一起。语义需要捕获信号处理和异常处理之间的复杂交互。

机械化语义学

Mechanized semantics

本讲座的目标是展示现代定理证明器--在本例中，Coq证明助手--如何用于机械化程序设计语言及其语义的规范，以及如何对单个程序和通用程序转换进行推理，如通常在编译器中发现的那样。所涵盖的主题包括：操作语义学（小步、大步、定义解释器）;指称语义的简单形式;公理语义学和霍尔逻辑;验证条件的生成，以及对程序证明的应用;编译成虚拟机器码及其正确性证明;优化程序转换（死代码消除）及其正确性证明的示例。