VeryFi Lambda

This project defines a simply-typed lambda calculus using Ott, defines a reference interpreter in Coq and proves it equivalent to the operational semantics in Ott, and extracts this verified interpreter to OCaml.

Dependencies

• Ott (v0.34) (the ott CLI) to generate system.v from system.ott.
• Coq (tested with Coq 8.19).
• OCaml (ocamlopt) for the extracted interpreter.
• Metalib: this development uses the locally-nameless infrastructure from Metalib.Metatheory.

Metalib.Metatheory

This repo expects Metalib to be available under the local path metalib/Metalib, and the build uses the Coq loadpath flag:

-Q metalib/Metalib Metalib

That flag is already wired into the top-level Makefile as COQFLAGS.

To get Metalib:

• If this repository includes the metalib/ folder already, you only need to compile Metalib once:

   make -C metalib/Metalib

• If you do not have metalib/ in your checkout, clone it into place:

   git clone https://github.com/plclub/metalib.git metalib
   make -C metalib/Metalib

After that, make coq (and the full make) should be able to Require Import Metalib.Metatheory..

Files

• system.ott - Ott specification of the lambda calculus syntax and semantics
• interpreter.v - Coq implementation of call-by-name interpreter with equivalence proofs
• extract.v - Coq extraction configuration for OCaml
• main.ml - OCaml driver program with tests
• Makefile - Build automation

Quick Start

First ensure Metalib is built (see above), then:

# Build everything and run tests
make

# Or step by step:
make ott      # Generate .v from .ott
make coq      # Compile Coq files
make extract  # Extract OCaml code
make ocaml    # Compile OCaml interpreter
make test     # Run tests

Workflow

1. Edit the Specification

Edit system.ott to modify the language definition. Then regenerate:

make ott

This will regenerate system.v.

2. Modify the Interpreter

Edit interpreter.v to change the interpreter implementation or add proofs.

3. Extract the Ocaml interpreter

make extract
make ocaml

4. Test

make test