Code Monkey home page Code Monkey logo

church-rossser's Introduction

This repository contains a formalization of part of Chapter 3 of H.P. Barendregt, "The Lambda Calculus, Its Syntax and Semantics".

The main result shown here is a proof of the Church-Rosser theorem for the untyped lambda calculus, that Barendregt attributes to Tait and Martin-Lof.

The goal of this formalization is an advanced tutorial on the use of Ott/LNgen for working with the locally nameless representation of variable binding. It is intended to follow the Stlc tutorial found in the Penn metalib repository.

To start the tutorial, read overview.md.

Compilation instructions

This development has been tested with The Coq Proof Assistant, version 8.17.0.

If you have Coq, Ott, metalib and LaTeX installed (see below), the toplevel Makefile supports the following targets:

`make coq`   - compile the coq development
    
`make spec`  - use Ott to generate LaTeX definitions and then produce
               the document [spec/lc.pdf](spec/lc.pdf)
              
`make gen`   - use Ott and LNgen to regenerate the two Coq files 
               listed below.
              
`make clean` - remove all generated files

The command make triggers the coq and spec targets.

Rules Specification

The specification of the lambda calculus grammar and associated inductive relations is in the Ott specification in lc.ott. The Makefile then uses this file to generate three files:

  • spec/lc-rules.tex, containing LaTeX definitions of the system. This file is imported by spec/lc.mng, a LaTeX file that is preprocessed by Ott to produce spec/lc.pdf.

  • coq/lc_ott.v, containing Coq definitions of the inductive datatypes specified in the system, and generated by Ott's locally nameless backend.

  • and coq/lc_inf.v, containing auxiliary Coq definitions (open, size, etc.) and proofs about the substitution and free variable functions, generated by LNgen.

These generated files are included in the repository in case you would like to work through the details without installing Ott or LNgen.

Tools installation

To compile this code with Coq, you also need to install a copy of the Metalib library. This library is available from https://github.com/plclub/metalib.

You can install these tools via opam (https://opam.ocaml.org/):

 opam switch create 4.11.1
 opam repo add coq-released https://coq.inria.fr/opam/released
 opam pin coq 8.15.0
 opam pin add coq-metalib https://github.com/plclub/metalib.git

To regenerate the Ott and LNgen definitions, you will need to install these tools separately. The former is available through opam.

 opam install ott

The LNgen tool can be cloned from its repository and built using Haskell.

church-rossser's People

Contributors

sweirich avatar

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    ๐Ÿ–– Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. ๐Ÿ“Š๐Ÿ“ˆ๐ŸŽ‰

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google โค๏ธ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.