Commit 9dcf1970 authored by Paul Wild's avatar Paul Wild

update README

parent ca5dad93
<h1>Logical Relations in Coq</h1> <h1>Logical Relations in Coq</h1>
<p>This project is an extension of the development in the ModuRes tutorial, mostly following <p>This project is an extension of the development in the ModuRes tutorial, mostly following
the exercises set at the end of chapter 3 (<code>Fmu.v</code>). Present in this project are three the exercises set at the end of chapter 3 (<code>Fmu.v</code>). The code from the project can be found
logical relations:</p> inside the <code>project/</code> directory, the other directories have been taken from the ModuRes
tutorial archive as-is*. The file <code>ModuResREADME.org</code> contains the readme from that archive.</p>
<p>*: Two lemmas were added in the file <code>dblib/Environments.v</code>: <code>subst_insert</code> and <code>lookup_lift</code>.</p>
<p>Present in this project are three logical relations:</p>
<ul> <ul>
<li>The first LR is an extension of the unary LR for type safety given in the tutorial, <li><p>The first LR is an extension of the unary LR for type safety given in the tutorial,
where unit, sum and existential types have been added, thus providing a solution for where unit, sum and existential types have been added, thus providing a solution for
the first two exercises. the first two exercises. For ease of reading, the documentation from the tutorial has
This LR can be found in the subdirectory <code>Unary</code>.</li> been kept, and new comments have been added wherever changes were made. To differentiate
<li>The second LR is binary and sound with respect to contextual approximation, between the two, all the text from the tutorial has been set in <em>italics</em>.
and is built for the same language. This LR can be found in the subdirectory <code>project/Unary/</code>.</p></li>
<li><p>The second LR is a binary LR that is sound with respect to contextual approximation,
and is built for the same language. The main source for this and the next part is
"Birkedal, Dreyer, Ahmed. Logical Step Indexed Logical Relations" (LSLR).
The soundness proof is provided and the LR is then used to prove two examples The soundness proof is provided and the LR is then used to prove two examples
of approximation: one involving two implementations of an abstract queue data type of approximation, one involving two implementations of an abstract queue data type
(file <code>Queues.v</code>) as well as a simple parametricity result (file <code>Parametricity.v</code>) (file <code>Queues.v</code>) as well as a simple parametricity result (file <code>Parametricity.v</code>)
This LR and the examples can be found in the subdirectory <code>Binary</code>.</li> This LR and the examples can be found in the subdirectory <code>project/Binary/</code>.</p></li>
<li>The third LR is also a binary LR for contextual approximation but it is more "complete": <li><p>The third LR is another binary LR for contextual approximation that is more "complete":
syntactic types are included right in the definition of the LR. This makes it possible syntactic types are included right in the definition of the LR. This makes it possible
to prove, for example, that terms that are logically related at some type are actually to prove, for example, that terms that are logically related at some type are actually
of that type. of that type, which then enables reasoning about their structure.
This LR is then used to prove one of the examples from the LSLR paper (file This LR is first proven to be sound and then used to prove one of the examples from
<code>SyntacticMinimalInvariance.v</code>, all of this can be found in the subdirectory <code>BinaryTyped</code>.</li> the LSLR paper (file <code>SyntacticMinimalInvariance.v</code>).
All of this can be found in the subdirectory <code>project/BinaryTyped/</code>.</p></li>
</ul> </ul>
<p>As all three LRs share the same language and many of the proofs have a similar structure, <p>As all three LRs share the same language and many of the proofs have a similar structure,
some definitions and tactics that are useful for all of them have been moved to the some definitions and tactics that are useful for all of them have been moved to the
top level directory and are imported appropriately. The full dependency graph is provided <code>Common/</code> subdirectory and are imported appropriately.
in <code>dependencies.png</code>. The intended order of reading is in a depth-first, left-to-right The full dependency graph can be seen below.</p>
order.</p>
<p><img src="project/dependencies.png" alt="dep" title="" /></p>
<p>All files have Coqdoc documentation explaining the most important parts of the development.
The intended way of reading through the files is in a depth-first, left-to-right order.
The files <code>Language.v</code>, <code>Lib.v</code> and <code>Tactics.v</code> can be found in the <code>Common/</code> subdirectory.</p>
<p>The table of contents can be found <a href="project/html/toc_sorted.html">here</a>.</p>
<h3>To build:</h3> <h3>To build:</h3>
<blockquote> <p>Run the commands</p>
<p><code>$ (cd dblib &amp;&amp; make)</code></p>
<pre><code>$ (cd dblib &amp;&amp; make)
$ (cd ModuRes &amp;&amp; make)
$ (cd project &amp;&amp; make)
</code></pre>
<p><code>$ (cd ModuRes &amp;&amp; make)</code></p> <p>The Coqdoc HTML files can be generated by running <code>make html</code> from the <code>project/</code> directory
and can then be found in <code>project/html/</code>.</p>
<p><code>$ (cd project &amp;&amp; make)</code></p> <p>The code has been tested with Coq version <code>8.4pl5</code>.</p>
</blockquote>
<h3>To run interactively:</h3> <h3>To run the proof scripts interactively:</h3>
<p>The project comes with a <code>_CoqProject</code> file that contains a list of all the necessary <p>The project comes with a <code>_CoqProject</code> file that contains a list of all the necessary
<code>-R</code> remappings. If you are using Proof General, it should autmatically apply them and <code>-R</code> remappings. If you are using Proof General, it should automatically apply them and
you should be able to run through the scripts in interactive mode. If you are using CoqIDE, you should be able to run through the scripts in interactive mode. If you are using CoqIDE,
you have to change the project file options in <code>Preferences &gt; Project</code> first to you have to first go to the project file options (<code>Preferences &gt; Project</code>) and then select
<code>taken instead of arguments</code>.</p> the option <em>taken instead of arguments</em> in the drop-down menu.</p>
# Logical Relations in Coq # Logical Relations in Coq
This project is an extension of the development in the ModuRes tutorial, mostly following This project is an extension of the development in the ModuRes tutorial, mostly following
the exercises set at the end of chapter 3 (`Fmu.v`). Present in this project are three the exercises set at the end of chapter 3 (`Fmu.v`). The code from the project can be found
logical relations: inside the `project/` directory, the other directories have been taken from the ModuRes
tutorial archive as-is\*. The file `ModuResREADME.org` contains the readme from that archive.
\*: Two lemmas were added in the file `dblib/Environments.v`: `subst_insert` and `lookup_lift`.
Present in this project are three logical relations:
- The first LR is an extension of the unary LR for type safety given in the tutorial, - The first LR is an extension of the unary LR for type safety given in the tutorial,
where unit, sum and existential types have been added, thus providing a solution for where unit, sum and existential types have been added, thus providing a solution for
the first two exercises. the first two exercises. For ease of reading, the documentation from the tutorial has
This LR can be found in the subdirectory `Unary`. been kept, and new comments have been added wherever changes were made. To differentiate
- The second LR is binary and sound with respect to contextual approximation, between the two, all the text from the tutorial has been set in *italics*.
and is built for the same language. This LR can be found in the subdirectory `project/Unary/`.
- The second LR is a binary LR that is sound with respect to contextual approximation,
and is built for the same language. The main source for this and the next part is
"Birkedal, Dreyer, Ahmed. Logical Step Indexed Logical Relations" (LSLR).
The soundness proof is provided and the LR is then used to prove two examples The soundness proof is provided and the LR is then used to prove two examples
of approximation: one involving two implementations of an abstract queue data type of approximation, one involving two implementations of an abstract queue data type
(file `Queues.v`) as well as a simple parametricity result (file `Parametricity.v`) (file `Queues.v`) as well as a simple parametricity result (file `Parametricity.v`)
This LR and the examples can be found in the subdirectory `Binary`. This LR and the examples can be found in the subdirectory `project/Binary/`.
- The third LR is also a binary LR for contextual approximation but it is more "complete":
- The third LR is another binary LR for contextual approximation that is more "complete":
syntactic types are included right in the definition of the LR. This makes it possible syntactic types are included right in the definition of the LR. This makes it possible
to prove, for example, that terms that are logically related at some type are actually to prove, for example, that terms that are logically related at some type are actually
of that type. of that type, which then enables reasoning about their structure.
This LR is then used to prove one of the examples from the LSLR paper (file This LR is first proven to be sound and then used to prove one of the examples from
`SyntacticMinimalInvariance.v`), all of this can be found in the subdirectory `BinaryTyped`. the LSLR paper (file `SyntacticMinimalInvariance.v`).
All of this can be found in the subdirectory `project/BinaryTyped/`.
As all three LRs share the same language and many of the proofs have a similar structure, As all three LRs share the same language and many of the proofs have a similar structure,
some definitions and tactics that are useful for all of them have been moved to the some definitions and tactics that are useful for all of them have been moved to the
top level directory and are imported appropriately. The full dependency graph is provided `Common/` subdirectory and are imported appropriately.
in `dependencies.png`. The intended order of reading is in a depth-first, left-to-right The full dependency graph can be seen below.
order.
![dep](project/dependencies.png)
All files have Coqdoc documentation explaining the most important parts of the development.
The intended way of reading through the files is in a depth-first, left-to-right order.
The files `Language.v`, `Lib.v` and `Tactics.v` can be found in the `Common/` subdirectory.
The table of contents can be found [here](project/html/toc_sorted.html).
### To build: ### To build:
> `$ (cd dblib && make)` Run the commands
> `$ (cd ModuRes && make)` $ (cd dblib && make)
$ (cd ModuRes && make)
$ (cd project && make)
> `$ (cd project && make)` The Coqdoc HTML files can be generated by running `make html` from the `project/` directory
and can then be found in `project/html/`.
### To run interactively: The code has been tested with Coq version `8.4pl5`.
### To run the proof scripts interactively:
The project comes with a `_CoqProject` file that contains a list of all the necessary The project comes with a `_CoqProject` file that contains a list of all the necessary
`-R` remappings. If you are using Proof General, it should autmatically apply them and `-R` remappings. If you are using Proof General, it should automatically apply them and
you should be able to run through the scripts in interactive mode. If you are using CoqIDE, you should be able to run through the scripts in interactive mode. If you are using CoqIDE,
you have to change the project file options in `Preferences > Project` first to you have to first go to the project file options (`Preferences > Project`) and then select
`taken instead of arguments`. the option *taken instead of arguments* in the drop-down menu.
...@@ -63,7 +63,7 @@ OPT?= ...@@ -63,7 +63,7 @@ OPT?=
COQDEP?=$(COQBIN)coqdep -c COQDEP?=$(COQBIN)coqdep -c
COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML) COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
COQCHKFLAGS?=-silent -o COQCHKFLAGS?=-silent -o
COQDOCFLAGS?=-s -interpolate -utf8 COQDOCFLAGS?=-interpolate -utf8
COQC?=$(COQBIN)coqc COQC?=$(COQBIN)coqc
GALLINA?=$(COQBIN)gallina GALLINA?=$(COQBIN)gallina
COQDOC?=$(COQBIN)coqdoc COQDOC?=$(COQBIN)coqdoc
......
...@@ -4,7 +4,6 @@ ...@@ -4,7 +4,6 @@
-R Unary Unary -R Unary Unary
-R Binary Binary -R Binary Binary
-R BinaryTyped BinaryTyped -R BinaryTyped BinaryTyped
#COQDOCFLAGS?="-interpolate -utf8"
Common/Language.v Common/Language.v
Common/Lib.v Common/Lib.v
Common/Tactics.v Common/Tactics.v
......
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="coqdoc.css" rel="stylesheet" type="text/css"/>
<title>Table of contents</title>
</head>
<body>
<div id="page">
<div id="header">
</div>
<div id="main">
<div id="toc">
<a href="Common.Language.html">Library Common.Language</a>
<ul class="doclist">
<li><a href="Common.Language.html#lab70">Chapter 0. Language and common definitions</a>
<ul class="doclist">
<li><a href="Common.Language.html#lab71">Language</a>
</li>
<li><a href="Common.Language.html#lab72">Type system and operational semantics</a>
</li>
<li><a href="Common.Language.html#lab73">Contexts</a>
</li>
</ul>
</li>
</ul>
<a href="Common.Lib.html">Library Common.Lib</a>
<ul class="doclist">
<li><ul class="doclist">
<li><a href="Common.Lib.html#lab67">Substitution lemmas</a>
</li>
<li><a href="Common.Lib.html#lab68">Closedness</a>
</li>
<li><a href="Common.Lib.html#lab69">Multi-Step</a>
</li>
</ul>
</li>
</ul>
<a href="Common.Tactics.html">Library Common.Tactics</a>
<ul class="doclist">
<li><ul class="doclist">
<li><a href="Common.Tactics.html#lab66">Type checker and interpreter tactics</a>
</li>
</ul>
</li>
</ul>
<a href="Unary.LogRel.html">Library Unary.LogRel</a>
<ul class="doclist">
<li><a href="Unary.LogRel.html#lab52">Chapter 1. A unary logical relation for type safety</a>
<ul class="doclist">
<li><a href="Unary.LogRel.html#lab53">Constructions</a>
<ul class="doclist">
<li><a href="Unary.LogRel.html#lab54">The type of the interpretation function</a>
</li>
<li><a href="Unary.LogRel.html#lab55">Combinators on <span class="inlinecode"><span class="id" type="var">int</span></span> <span class="inlinecode"><span class="id" type="var">k</span></span></a>
<ul class="doclist">
<li><a href="Unary.LogRel.html#lab56">Natural numbers</a>
</li>
<li><a href="Unary.LogRel.html#lab57">Unit</a>
</li>
<li><a href="Unary.LogRel.html#lab58">Products</a>
</li>
<li><a href="Unary.LogRel.html#lab59">Sums</a>
</li>
<li><a href="Unary.LogRel.html#lab60">Functions</a>
</li>
<li><a href="Unary.LogRel.html#lab61">Type variables</a>
</li>
<li><a href="Unary.LogRel.html#lab62">Universal types</a>
</li>
<li><a href="Unary.LogRel.html#lab63">Existential types</a>
</li>
<li><a href="Unary.LogRel.html#lab64">Recursive types</a>
</li>
</ul>
</li>
</ul>
</li>
<li><a href="Unary.LogRel.html#lab65">Interpretation</a>
</li>
</ul>
</li>
</ul>
<a href="Unary.WeakSub.html">Library Unary.WeakSub</a>
<ul class="doclist">
<li><ul class="doclist">
<li><a href="Unary.WeakSub.html#lab49">Properties of the Interpretation</a>
<ul class="doclist">
<li><a href="Unary.WeakSub.html#lab50">Weakening and substitution</a>
</li>
<li><a href="Unary.WeakSub.html#lab51">Properties of the Environments</a>
</li>
</ul>
</li>
</ul>
</li>
</ul>
<a href="Unary.Compatibility.html">Library Unary.Compatibility</a>
<ul class="doclist">
<li><ul class="doclist">
<li><a href="Unary.Compatibility.html#lab46">Compatibility Lemmas</a>
</li>
<li><a href="Unary.Compatibility.html#lab47">Fundamental Lemma</a>
</li>
<li><a href="Unary.Compatibility.html#lab48">Towards Soundness</a>
</li>
</ul>
</li>
</ul>
<a href="Binary.LogRel.html">Library Binary.LogRel</a>
<ul class="doclist">
<li><a href="Binary.LogRel.html#lab32">Chapter 2. A binary logical relation for contextual approximation</a>
<ul class="doclist">
<li><a href="Binary.LogRel.html#lab33">Constructions</a>
<ul class="doclist">
<li><a href="Binary.LogRel.html#lab34">The type of the interpretation function</a>
</li>
<li><a href="Binary.LogRel.html#lab35">Combinators on <span class="inlinecode"><span class="id" type="var">int</span></span> <span class="inlinecode"><span class="id" type="var">k</span></span></a>
<ul class="doclist">
<li><a href="Binary.LogRel.html#lab36">Natural numbers</a>
</li>
<li><a href="Binary.LogRel.html#lab37">Unit</a>
</li>
<li><a href="Binary.LogRel.html#lab38">Products</a>
</li>
<li><a href="Binary.LogRel.html#lab39">Sums</a>
</li>
<li><a href="Binary.LogRel.html#lab40">Functions</a>
</li>
<li><a href="Binary.LogRel.html#lab41">Type variables</a>
</li>
<li><a href="Binary.LogRel.html#lab42">Universal types</a>
</li>
<li><a href="Binary.LogRel.html#lab43">Existential types</a>
</li>
<li><a href="Binary.LogRel.html#lab44">Recursive types</a>
</li>
</ul>
</li>
</ul>
</li>
<li><a href="Binary.LogRel.html#lab45">Interpretation</a>
</li>
</ul>
</li>
</ul>
<a href="Binary.WeakSub.html">Library Binary.WeakSub</a>
<ul class="doclist">
<li><ul class="doclist">
<li><a href="Binary.WeakSub.html#lab29">Properties of the interpretation</a>
<ul class="doclist">
<li><a href="Binary.WeakSub.html#lab30">Weakening and substitution</a>
</li>
<li><a href="Binary.WeakSub.html#lab31">Properties of the Environments</a>
</li>
</ul>
</li>
</ul>
</li>
</ul>
<a href="Binary.Compatibility.html">Library Binary.Compatibility</a>
<ul class="doclist">
<li><ul class="doclist">
<li><a href="Binary.Compatibility.html#lab26">Compatibility lemmas</a>
</li>
<li><a href="Binary.Compatibility.html#lab27">Fundamental Lemma</a>
</li>
<li><a href="Binary.Compatibility.html#lab28">Soundness</a>
</li>
</ul>
</li>
</ul>
<a href="Binary.Parametricity.html">Library Binary.Parametricity</a>
<ul class="doclist">
<li><ul class="doclist">
<li><a href="Binary.Parametricity.html#lab24">A parametricity result</a>
</li>
</ul>
</li>
</ul>
<a href="Binary.QueueDefinitions.html">Library Binary.QueueDefinitions</a>
<ul class="doclist">
<li><ul class="doclist">
<li><ul class="doclist">
<li><a href="Binary.QueueDefinitions.html#lab25">Definitions</a>
</li>
</ul>
</li>
</ul>
</li>
</ul>
<a href="Binary.Queues.html">Library Binary.Queues</a>
<a href="BinaryTyped.WeakSubSyntactic.html">Library BinaryTyped.WeakSubSyntactic</a>
<ul class="doclist">
<li><a href="BinaryTyped.WeakSubSyntactic.html#lab22">Chapter 3. Another binary logical relation</a>
<ul class="doclist">
<li><a href="BinaryTyped.WeakSubSyntactic.html#lab23">Syntactic Weakening and Substitution Properties</a>
</li>
</ul>
</li>
</ul>
<a href="BinaryTyped.LogRel.html">Library BinaryTyped.LogRel</a>
<ul class="doclist">
<li><ul class="doclist">
<li><a href="BinaryTyped.LogRel.html#lab8">Constructions</a>
<ul class="doclist">
<li><a href="BinaryTyped.LogRel.html#lab9">The type of the interpretation function</a>
</li>
</ul>
</li>
<li><a href="BinaryTyped.LogRel.html#lab10">From Semantic to syntactic type variable contexts</a>
<ul class="doclist">
<li><a href="BinaryTyped.LogRel.html#lab11">Combinators on <span class="inlinecode"><span class="id" type="var">int</span></span> <span class="inlinecode"><span class="id" type="var">k</span></span></a>
<ul class="doclist">
<li><a href="BinaryTyped.LogRel.html#lab12">Natural numbers</a>
</li>
<li><a href="BinaryTyped.LogRel.html#lab13">Unit</a>
</li>
<li><a href="BinaryTyped.LogRel.html#lab14">Products</a>
</li>
<li><a href="BinaryTyped.LogRel.html#lab15">Sums</a>
</li>
<li><a href="BinaryTyped.LogRel.html#lab16">Functions</a>
</li>
<li><a href="BinaryTyped.LogRel.html#lab17">Type variables</a>
</li>
<li><a href="BinaryTyped.LogRel.html#lab18">Universal types</a>
</li>
<li><a href="BinaryTyped.LogRel.html#lab19">Existential types</a>
</li>
<li><a href="BinaryTyped.LogRel.html#lab20">Recursive types</a>
</li>
</ul>
</li>
</ul>
</li>
<li><a href="BinaryTyped.LogRel.html#lab21">Interpretation</a>
</li>
</ul>
</li>
</ul>
<a href="BinaryTyped.WeakSub.html">Library BinaryTyped.WeakSub</a>
<ul class="doclist">
<li><ul class="doclist">
<li><a href="BinaryTyped.WeakSub.html#lab5">Properties of the interpretation</a>
<ul class="doclist">
<li><a href="BinaryTyped.WeakSub.html#lab6">Weakening and substitution</a>
</li>
<li><a href="BinaryTyped.WeakSub.html#lab7">Properties of the Environments</a>
</li>
</ul>
</li>
</ul>
</li>
</ul>
<a href="BinaryTyped.Compatibility.html">Library BinaryTyped.Compatibility</a>
<ul class="doclist">
<li><ul class="doclist">
<li><a href="BinaryTyped.Compatibility.html#lab2">Compatibility lemmas</a>
</li>
<li><a href="BinaryTyped.Compatibility.html#lab3">Fundamental Lemma</a>
</li>
<li><a href="BinaryTyped.Compatibility.html#lab4">Soundness</a>
</li>
</ul>
</li>
</ul>
<a href="BinaryTyped.SyntacticMinimalInvariance.html">Library BinaryTyped.SyntacticMinimalInvariance</a>
<ul class="doclist">
<li><ul class="doclist">
<li><a href="BinaryTyped.SyntacticMinimalInvariance.html#lab1">Syntactic Minimal Invariance</a>
</li>
</ul>
</li>
</ul>
</div>
<hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
</div>
</div>
</body>
</html>
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment