-
Notifications
You must be signed in to change notification settings - Fork 13
/
Copy pathmeta.yml
226 lines (200 loc) · 9.38 KB
/
meta.yml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
fullname: Monadic effects and equational reasoning in Coq
shortname: monae
organization: affeldt-aist
opam_name: coq-monae
community: false
action: true
coqdoc: false
synopsis: >-
Monads and equational reasoning in Coq
description: |-
This Coq library contains a hierarchy of monads with their laws used
in several examples of monadic equational reasoning.
authors:
- name: Reynald Affeldt
initial: true
- name: David Nowak
initial: true
- name: Takafumi Saikawa
initial: true
- name: Jacques Garrigue
initial: false
- name: Ayumu Saito
initial: false
- name: Celestine Sauvage
initial: false
- name: Kazunari Tanaka
initial: false
opam-file-maintainer: Reynald Affeldt <[email protected]>
license:
fullname: LGPL-2.1-or-later
identifier: LGPL-2.1-or-later
file: LICENSE
supported_coq_versions:
text: Coq 8.19-8.20
opam: '{ (>= "8.19" & < "8.21~") | (= "dev") }'
tested_coq_opam_versions:
- version: '2.3.0-coq-8.19'
repo: 'mathcomp/mathcomp'
- version: '2.3.0-coq-8.20'
repo: 'mathcomp/mathcomp'
dependencies:
- opam:
name: coq-mathcomp-ssreflect
version: '{ (>= "2.3.0") }'
description: |-
[MathComp ssreflect](https://math-comp.github.io)
- opam:
name: coq-mathcomp-fingroup
version: '{ (>= "2.3.0") }'
description: |-
[MathComp fingroup](https://math-comp.github.io)
- opam:
name: coq-mathcomp-algebra
version: '{ (>= "2.3.0") }'
description: |-
[MathComp algebra](https://math-comp.github.io)
- opam:
name: coq-mathcomp-solvable
version: '{ (>= "2.3.0") }'
description: |-
[MathComp solvable](https://math-comp.github.io)
- opam:
name: coq-mathcomp-field
version: '{ (>= "2.3.0") }'
description: |-
[MathComp field](https://math-comp.github.io)
- opam:
name: coq-mathcomp-analysis
version: '{ (>= "1.8.0") }'
description: |-
[MathComp analysis](https://github.com/math-comp/analysis)
- opam:
name: coq-infotheo
version: '{ >= "0.7.6"}'
description: |-
[Infotheo](https://github.com/affeldt-aist/infotheo)
- opam:
name: coq-paramcoq
version: '{ >= "1.1.3" & < "1.2~" }'
description: |-
[Paramcoq](https://github.com/coq-community/paramcoq)
- opam:
name: coq-hierarchy-builder
version: '{ >= "1.7.0" }'
description: |-
[Hierarchy Builder](https://github.com/math-comp/hierarchy-builder)
- opam:
name: coq-equations
version: '{ >= "1.3" & < "1.4~" }'
description: |-
[Coq-Equations](https://github.com/mattam82/Coq-Equations)
namespace: monae
keywords:
- name: monae
- name: effects
- name: probability
- name: nondeterminism
#date:
#- 2021-02-21
publications:
- pub_url: https://staff.aist.go.jp/reynald.affeldt/documents/monae.pdf
pub_title: A hierarchy of monadic effects for program verification using equational reasoning
pub_doi: 10.1007/978-3-030-33636-3_9
- pub_url: https://drops.dagstuhl.de/opus/volltexte/2021/13881/
pub_title: Extending Equational Monadic Reasoning with Monad Transformers
pub_doi: 10.4230/LIPIcs.TYPES.2020.2
- pub_url: https://arxiv.org/abs/2003.09993
pub_title: A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism
pub_doi: 10.1017/S0956796821000137
- pub_url: https://staff.aist.go.jp/reynald.affeldt/documents/monae-mpc2022.pdf
pub_title: Towards a practical library for monadic equational reasoning in Coq
pub_doi: 10.1007/978-3-031-16912-0_6
- pub_url: https://coq-workshop.gitlab.io/2023/abstracts/coq2023_monadic-reasoning.pdf
pub_title: Environment-friendly monadic equational reasoning for OCaml
#make_target: [
# [make "-j%{jobs}%"]
# [make "-C" "impredicative_set"]
#]
#
#install: [ [make "install_full"] ]
build: |-
## Building and installation instructions
The easiest way to install the latest released version of Monadic effects and equational reasoning in Coq
is via [OPAM](https://opam.ocaml.org/doc/Install.html):
```shell
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-monae
```
It installs two directories in `coq/user-contrib`: `monae` and
`monaeImpredicativeSet`.
To instead build and install manually (with GNU `make`), do:
``` shell
git clone https://github.com/affeldt-aist/monae.git
cd monae
make -j 4
make install
```
documentation: |-
## Overview
This repository contains a formalization of monads including examples
of monadic equational reasoning and several models. This includes for
example the formalization of the following papers:
- [Gibbons and Hinze, Just do It: Simple Monadic Equational Reasoning, ICFP 2011] (except Sect. 10.2)
- [Gibbons, Unifying Theories of Programming with Monads, UTP 2012] (up to Sect. 7.2)
- [Mu, Equational Reasoning for Non-determinism Monad: A Case study of Spark Aggregation, TR-IIS-19-002, Academia Sinica]
- [Mu, Calculating a Backtracking Algorithm: An exercise in Monadic Program Derivation, TR-IIS-29-003, Academia Sinica]
- [Mu, Functional Pearls: Reasoning and Derivation of Monadic Programs, A case study of non-determinism and state, 2017]
+ This is a draft paper. In the first release, we formalized this draft up to Sect. 5.
The contents have been since superseded by [mu2019tr2] and [mu2019tr3].
- [Mu and Chiang, Deriving Monadic Quicksort (Declarative Pearl), 2020]
This library has been applied to other formalizations:
- application to program semantics (see file `smallstep.v`)
- formalization of monad composition [Jones and Duponcheel, Composing Monads, Yale RR 1993] (Sections 2 and 3)
- formalization of monad transformers [Jaskelioff, Modular Monad Transformers, ESOP 2009] (up to Sect. 4)
+ completed with details from [Jaskelioff, Lifting of Operations in Modular Monadic Semantics, PhD 2009]
+ see directory `impredicative_set` for the formalization of [Jaskelioff, Modular Monad Transformers, ESOP 2009] (from Sect. 5)
- formalization of the geometrically convex monad (main reference:
[Cheung, Distributive Interaction of Algebraic Effects, PhD Thesis, U. Oxford, 2017])
## Files
- core:
+ [preamble.v](./theories/core/preamble.v): simple additions to base libraries
+ [hierarchy.v](./theories/core/hierarchy.v): hierarchy of monadic effects
+ [category.v](./theories/core/category.v): formalization of concrete categories (generalization of the bottom layers of `hierarchy.v`)
+ [monad_transformer.v](./theories/core/monad_transformer.v): monad transformers
* completed by `ifmt_lifting.v` and `iparametricty_codensity.v` in the directory `impredicative_set`
- the directory `impredicative_set` contains a lighter version of Monae where monads live in `Set` and that compiles with `impredicative-set`
- libraries for each monad theory:
+ [monad_lib.v](./theories/lib/monad_lib.v): basic lemmas about monads
+ [fail_lib.v](./theories/lib/fail_lib.v): lemmas about the fail monad and related monads
+ [state_lib.v](./theories/lib/state_lib.v): lemmas about state-related monads
+ [array_lib.v](./theories/lib/array_lib.v): lemmas about the array monad
+ [trace_lib.v](./theories/lib/trace_lib.v): lemmas about about the state-trace monad
+ [proba_lib.v](./theories/lib/proba_lib.v): lemmas about the probability monad
+ [typed_store_lib.v](./theories/lib/typed_store_lib.v): derived definitions and lemmas about about the typed store monad
- models of monads:
+ [monad_model.v](./theories/models/monad_model.v): concrete models of monads
+ [proba_monad_model.v](./theories/models//proba_monad_model.v): model of the probability monad
+ [gcm_model.v](./theories/models//gcm_model.v): model of the geometrically convex monad
+ [altprob_model.v](./theories/models//altprob_model.v): model of a monad that mixes non-deterministic choice and probabilistic choice
+ [typed_store_model.v](./theories/models//typed_store_model.v): alternative model of the typed store monad
- applications:
+ [example_relabeling.v](./theories/applications/example_relabeling.v): tree relabeling
+ [example_monty.v](./theories/applications/example_monty.v): Monty Hall problem
+ [example_spark.v](./theories/applications/example_spark.v): Spark aggregation
+ [example_iquicksort.v](./theories/applications/example_iquicksort.v): in-place quicksort
+ [example_quicksort.v](./theories/applications/example_quicksort.v): functional quicksort
+ [example_nqueens.v](./theories/applications/example_nqueens.v): the n-queens puzzle
+ [example_typed_store.v](./theories/applications/example_typed_store.v): ML programs with references
+ [example_transformer.v](./theories/applications/example_transformer.v): monad transformers
+ [smallstep.v](./theories/applications/smallstep.v): semantics for an imperative language, with equivalence operational semantics/denotation and sample imperative programs
+ [monad_composition.v](./theories/applications/monad_composition.v): composing monads
+ [category_ext.v](./theories/applications/category_ext.v): experimental library about categories
## About Installation with Windows 11
Installation of monae on Windows is less simple.
First install infotheo following the [instructions for Windows 11](https://github.com/affeldt-aist/infotheo).
Once infotheo is installed (with opam), do:
- `opam install coq-monae` or `git clone [email protected]:affeldt-aist/monae.git; opam install .`
## Original License
Before version 0.2, monae was distributed under the terms of the `GPL-3.0-or-later` license