iris-simp-lang
所属分类：collect
开发工具：Coq
文件大小：0KB
下载次数：0
上传日期：2023-05-17 04:11:12
上 传 者：
sh-1993
说明： 我们定义了一种简单的编程语言simp_lang，然后实例化Iris以验证具有并发分离的简单simp_lang程序...，
(We define a simple programming language, simp_lang, then instantiate Iris to verify simple simp_lang programs with concurrent separation logic.)
文件列表:
LICENSE (1067, 2023-12-27)
Makefile (826, 2023-12-27)
_CoqProject (381, 2023-12-27)
iris-simp-lang.opam (808, 2023-12-27)
src/ (0, 2023-12-27)
src/adequacy.v (2840, 2023-12-27)
src/class_instances.v (4640, 2023-12-27)
src/examples/ (0, 2023-12-27)
src/examples/par.v (1139, 2023-12-27)
src/examples/parallel_add.v (3820, 2023-12-27)
src/examples/spawn.v (3051, 2023-12-27)
src/examples/swap.v (497, 2023-12-27)
src/heap_lib.v (4211, 2023-12-27)
src/heap_ra.v (14361, 2023-12-27)
src/lang.v (20280, 2023-12-27)
src/notation.v (4704, 2023-12-27)
src/primitive_laws.v (7137, 2023-12-27)
src/proofmode.v (9780, 2023-12-27)
src/simp.v (260, 2023-12-27)
src/tactics.v (2599, 2023-12-27)
tutorial/ (0, 2023-12-27)
tutorial/slides/ (0, 2023-12-27)
tutorial/slides/simp_lang.003.png (100556, 2023-12-27)
tutorial/slides/simp_lang.005.png (214719, 2023-12-27)
tutorial/slides/simp_lang.008.png (100210, 2023-12-27)
tutorial/slides/simp_lang.009.png (194347, 2023-12-27)
tutorial/slides/simp_lang.010.png (191762, 2023-12-27)
tutorial/slides/simp_lang.015.png (188228, 2023-12-27)
tutorial/slides/simp_lang.017.png (100420, 2023-12-27)
tutorial/slides/simp_lang.018.png (210743, 2023-12-27)
tutorial/slides/simp_lang.019.png (206083, 2023-12-27)
# simp_lang
[](https://github.com/tchajed/iris-simp-lang/actions/workflows/build.yml)
simp_lang is a very simple programming language that we instantiate Iris with.
On top of that Iris gives a program logic based on weakest preconditions. It is
heavily inspired by heap_lang (and mostly copied from it) but aims to simplify
things down as much as possible while still supporting verifying concurrent
programs.
You might want to start with a [high-level conceptual
overview](https://youtu.be/HndwyM04KEU) (links to a YouTube video; if you'd
prefer there's a [static version](tutorial/)):
[](https://youtu.be/HndwyM04KEU)
This overview might be useful before diving into this code, which works out all
the details and goes a step beyond by also doing some program verification in our
new language.
The recommended reading order for this tutorial is the following:
1. [lang.v](src/lang.v) defines the syntax and semantics of simp_lang (instantiating `ectxi_language`)
2. [primitive_laws.v](src/primitive_laws.v) defines a _state interpretation_
for simp_lang (instantiating
`irisG simp_lang`). This is the connection between the state of simp_lang (a
heap from locations to values) and the Iris logic.
3. [heap_ra.v](src/heap_ra.v) and [heap_lib.v](src/heap_lib.v) are the mechanism for the state interpretation,
which will make more sense after seeing them used.
4. [adequacy.v](src/adequacy.v) sets up the generic language adequacy theorem
with an initialization of the state interpretation for simp_lang.
Next, you can check out some examples from the [Iris POPL 2021 tutorial](https://gitlab.mpi-sws.org/iris/tutorial-popl21/) that are
re-implemented and verified in simp_lang:
1. [examples/swap.v](src/examples/swap.v) verifies a version of swap.
2. [examples/parallel_add.v](src/examples/parallel_add.v) verifies the parallel
increment example. It also demonstrates applying the adequacy theorem to
derive a theorem about `parallel_add` whose statement is independent of Iris.
There are a few files that are optional reading which make the tutorial work:
- [tactics.v](src/tactics.v) and
[class_instances.v](src/class_instances.v) are necessary parts of the
implementation but aren't directly related to instantiating Iris.
- [notation.v](src/notation.v) makes it possible to write programs in simp_lang
- [proofmode.v](src/proofmode.v) gives enough proofmode support to actually
verify programs written in simp_lang.
- [examples/spawn.v](src/examples/spawn.v) and
[examples/par.v](src/examples/par.v) implement and verify the par combinator
(`e1 ||| e2`) used in the tutorial example.
## Compiling
This development relies on a development version of Iris and Coq 8.14 or later.
We test Coq 8.14, 8.15, 8.16, and master with Iris dev in CI. (The released
version of Iris is currently incompatible.)
You'll need to install Iris, which is easiest done through opam. There are
installation instructions at https://gitlab.mpi-sws.org/iris/iris.
近期下载者：
相关文件：
收藏者：