Skip to content

AEC.md

Latest commit

 

History

History
138 lines (114 loc) · 14.5 KB

AEC.md

File metadata and controls

138 lines (114 loc) · 14.5 KB

Artifact Evaluation Instructions

This is the artifact instructions for POPL 26 paper Big-Stop Semantics. The artifact contains Agda formalizations of theorems presented in the paper.

Download, installation, and sanity-testing

Local development

One can install Agda and its standard library from scratch, following the instructions:

  1. Install Agda v2.8.0 (instructions).
  2. Install the standard library v2.3 (instructions).

If the reviewer is already an Agda user (e.g. has Agda installed on their local machine), they will very likely have local environment that runs this artifact out-of-box, without any further installation. In particular, this artifact has been tested against the following Agda and standard library versions:

Agda Version Standard Library Version
2.8.0 2.3
2.7.0.1 2.1.1 / 2.2
2.6.4.3 2.0
2.6.4.1 2.0

To sanity check, locate and unzip stop.zip. Run the following command to load the entire artifact.

agda src/Index.agda

Alternatively using Emacs or VS Code with Agda emacs mode, open src/Index.agda and load the file by via C-c C-l (pressing Ctrl-C immediately followed by Ctrl-L). Depending on the spec of one's local machine, this step should take less than two minutes.

List of claims

The table below links the Agda formalization to the corresponding parts of the paper.
Each row identifies a definition or theorem proved in the paper and its formal counterpart in the artifact:

  • Section: where the claim appears in the paper.
  • Item: definition, lemma, or theorem in the paper.
  • File: the Agda source file containing the formalization.
  • Name: the specific definition, lemma, or theorem name within the file.

Together, these entries provide a complete mapping between the text of the paper and its mechanized proofs.

Section Item File Name Notes
§2.1 Syntax of call-by-value PCF Language.PCF _⊢_ and _val Figure 1 and 28
§2.2 Small-step semantics Language.SmallStep _↦_↝_ and _↦*_↝_ Figure 2, 3 and 6
§2.3 Big-step semantics Language.BigStep _⇓_↝_ Figure 4 and 7
§3, §6.1 Stack machine semantics Language.StackMachine _↦_↝_ and _↦*_↝_ Figure 10 and 11
§4, §5 Big-stop semantics Language.BigStop _⇩_↝_ Figure 8
§4.2 Lemma 13 Language.Progress progressing-progress Effectful version of lemma 13
§5 Lemma 14 SoundnessCompleteness.SmallStepBigStep ↦*⇔⇓
§5.1 Theorem 15 SoundnessCompleteness.BigStepBigStop ⇓⇔⇩
§5.1 Theorem 16 SoundnessCompleteness.SmallStepBigStop ↦*⇔⇩
§5.1 Lemma 17 Language.BigStop ⇩-trans
§5.1 Theorem 18 Language.Progress progress
§6.2 Lemma 19 SoundnessCompleteness.StackMachineBigStop ↦*→⇩-ε
§6.2 Lemma 20 SoundnessCompleteness.StackMachineBigStop ↦*→⇩s-ε
§6.2 Lemma 21 SoundnessCompleteness.StackMachineBigStop ⇩→↦*-ε
§6.2 Lemma 22 SoundnessCompleteness.StackMachineBigStop ⇩→↦*s-ε
Soundness Completeness
Convergent
Lemma 19		 Divergent
Lemma 20		 Convergent
Lemma 21		 Divergent
Lemma 22
Big-stop 76 72 32 72
↦*→⇩-ε ↦*→⇩s-ε ⇩→↦*-ε ⇩→↦*s-ε
Big-step 81 – 29 –
↦*→⇓-ε ⇓→↦*-ε
Small-step 88 84 68 128
↦*→⇒*-ε ↦*→⇒*s-ε ⇒*→↦*-ε ⇒*→↦*s-ε

Table 2: Lines of non-blank, non-comment code of soundness and completeness theorems of stack machine.

Evaluation instructions

The correctness criteria of this artifact is that the Agda code type-checks without errors. This means running agda src/Index.agda should complete without any errors.

Reviewers should also be able to interactively view the source code with syntax highlighting in the browser using the HTML functionality of Agda, to check the correspondence between Agda code and on-paper theorems. HTML files can be generated by running:

agda --html --html-dir=html src/Index.agda

The same html files are also available online at https://www.cs.cmu.edu/~runmingl/stop/.

Additional artifact description

Project Structure

The file structure included is as follows:

├── AEC.md
├── README.md
├── src
│   ├── Index.agda
│   ├── Prelude.agda
│   ├── Language
│   │   ├── BigStep.agda
│   │   ├── BigStop.agda
│   │   ├── PCF.agda
│   │   ├── Progress.agda
│   │   ├── SmallStep.agda
│   │   ├── StackMachine.agda
│   │   └── Substitution.agda
│   └── SoundnessCompleteness
│       ├── BigStepBigStop.agda
│       ├── SmallStepBigStep.agda
│       ├── SmallStepBigStop.agda
│       ├── StackMachineBigStep.agda
│       ├── StackMachineBigStop.agda
│       └── StackMachineSmallStep.agda
├── stop.agda-lib

Notations

Throughout the project, we take full advantage of Agda’s excellent support for infix operators to make the code read as naturally as it does on paper. Here are the key notations used:

Judgment Meaning
Γ ⊢ τ Typing judgment: term of type τ in context Γ.
v val Judgment that v is a value.
e ⇓ v ↝ a Big-step evaluation: e evaluates to value v with effect a.
e ↦* e' ↝ a Small-step evaluation: e steps to e' with effect a.
k ▹ e ↦* k' ◃ e' ↝ a Stack-machine evaluation: state k ▹ e steps to k' ◃ e' with effect a.
e ⇩ e' ↝ a Big-Stop evaluation: e stops at e' with effect a.
e ↧ e' ↝ a Progressing Big-Stop evaluation: e progresses to e' with effect a.