-
Notifications
You must be signed in to change notification settings - Fork 15
/
meta.yml
205 lines (172 loc) · 6.75 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
fullname: A Coq formalization of information theory and linear error correcting codes
shortname: infotheo
organization: affeldt-aist
opam_name: coq-infotheo
community: false
action: true
coqdoc: false
synopsis: >-
Discrete probabilities and information theory for Coq
description: |-
Infotheo is a Coq library for reasoning about discrete probabilities,
information theory, and linear error-correcting codes.
authors:
- name: Reynald Affeldt, AIST
initial: true
- name: Manabu Hagiwara, Chiba U. (previously AIST)
initial: true
- name: Jonas Senizergues, ENS Cachan (internship at AIST)
initial: true
- name: Jacques Garrigue, Nagoya U.
initial: false
- name: Kazuhiko Sakaguchi, Tsukuba U.
initial: false
- name: Taku Asai, Nagoya U. (M2)
initial: false
- name: Takafumi Saikawa, Nagoya U.
initial: false
- name: Naruomi Obata, Titech (M2)
initial: false
- name: Alessandro Bruni, IT-University of Copenhagen
initial: false
opam-file-maintainer: Reynald Affeldt <reynald.affeldt@aist.go.jp>
#opam-file-version: dev
license:
fullname: LGPL-2.1-or-later
identifier: LGPL-2.1-or-later
file: LICENSE
nix: true
supported_coq_versions:
text: Coq 8.19--8.20
opam: '{ (>= "8.19" & < "8.21~") | (= "dev") }'
tested_coq_opam_versions:
- version: '2.2.0-coq-8.19'
repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.20'
repo: 'mathcomp/mathcomp'
dependencies:
- opam:
name: coq-mathcomp-ssreflect
version: '{ (>= "2.2.0") | (= "dev") }'
description: |-
[MathComp ssreflect](https://math-comp.github.io)
- opam:
name: coq-mathcomp-fingroup
version: '{ (>= "2.2.0") | (= "dev") }'
description: |-
[MathComp fingroup](https://math-comp.github.io)
- opam:
name: coq-mathcomp-algebra
version: '{ (>= "2.2.0") | (= "dev") }'
description: |-
[MathComp algebra](https://math-comp.github.io)
- opam:
name: coq-mathcomp-solvable
version: '{ (>= "2.2.0") | (= "dev") }'
description: |-
[MathComp solvable](https://math-comp.github.io)
- opam:
name: coq-mathcomp-field
version: '{ (>= "2.2.0") | (= "dev") }'
description: |-
[MathComp field](https://math-comp.github.io)
- opam:
name: coq-mathcomp-analysis
version: '{ (>= "1.5.0") }'
description: |-
[MathComp analysis](https://github.com/math-comp/analysis)
- opam:
name: coq-hierarchy-builder
version: '{ >= "1.5.0" }'
description: |-
[Hierarchy Builder](https://github.com/math-comp/hierarchy-builder)
- opam:
name: coq-mathcomp-algebra-tactics
version: '{ >= "1.2.0" }'
description: |-
MathComp algebra tactics
- opam:
name: coq-interval
version: '{ >= "4.10.0"}'
description:
A Coq tactic for proving bounds
namespace: infotheo
keywords:
- name: information theory
- name: probability
- name: error-correcting codes
- name: convexity
publications:
- pub_title: "Robust Mean Estimation by All Means (short paper)"
- pub_url: https://dl.acm.org/doi/abs/10.1145/3479394.3479412
pub_title: "Trimming Data Sets: a Verified Algorithm for Robust Mean Estimation"
pub_doi: 10.1145/3479394.3479412
- pub_url: https://arxiv.org/abs/2004.12713
pub_title: Formal Adventures in Convex and Conical Spaces
pub_doi: 10.1007/978-3-030-53518-6_2
- pub_url: https://link.springer.com/article/10.1007/s10817-019-09538-8
pub_title: A Library for Formalization of Linear Error-Correcting Codes
pub_doi: 10.1007/s10817-019-09538-8
- pub_url: https://www.jstage.jst.go.jp/article/jssst/37/3/37_3_79/_article/-char/en
pub_title: Reasoning with Conditional Probabilities and Joint Distributions in Coq
pub_doi: 10.11309/jssst.37.3_79
- pub_url: http://staff.aist.go.jp/reynald.affeldt/documents/compression-isita2018.pdf
pub_title: Examples of formal proofs about data compression
pub_doi: 10.23919/ISITA.2018.8664276
- pub_url: http://staff.aist.go.jp/reynald.affeldt/documents/rs_isita2016_author_version.pdf
pub_title: Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes
- pub_url: http://staff.aist.go.jp/reynald.affeldt/documents/eccITP2015_authorsversion.pdf
pub_title: Formalization of error-correcting codes---from Hamming to modern coding theory
pub_doi: 10.1007/978-3-319-22102-1_2
- pub_url: https://link.springer.com/article/10.1007%2Fs10817-013-9298-1
pub_title: Formalization of Shannon’s Theorems
pub_doi: 10.1007/s10817-013-9298-1
#make_target: [
# [make "-j%{jobs}%" ]
# [make "-C" "extraction" "tests"] {with-test}
# ]
build: |-
## Building and installation instructions
The easiest way to install the latest released version of A Coq formalization of information theory and linear error correcting codes
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-infotheo
```
To instead build and install manually, do (using GNU `make`):
``` shell
git clone https://github.com/affeldt-aist/infotheo.git
cd infotheo
make # or make -j <number-of-cores-on-your-machine>
make -C extraction tests
make install
```
documentation: |-
## Acknowledgments
Many thanks to several [contributors](https://github.com/affeldt-aist/infotheo/graphs/contributors).
The principle of inclusion-exclusion is a contribution by
Erik Martin-Dorel (University Toulouse III Paul Sabatier, IRIT research laboratory)
(main theorem: Pr_bigcup_incl_excl; commit 956096859ed89325b2bb74033690ac882bbcd64e)
The variable-length source coding theorems are a contribution by
Ryosuke Obi (Chiba U. (M2))
(commit a67da5e24eaaabb345d225a5bd0f5e86d35413a8)
(with Manabu Hagiwara and Mitsuharu Yamamoto)
Commit 64814f529c1819684c4b8060d0779c24c6339041 was originally by Karl Palmskog
The formalization of modern coding theory is a collaboration with
K. Kasai, S. Kuzuoka, R. Obi
Y. Takahashi collaborated to the formalization of linear error-correcting codes
This work was partially supported by a JSPS Grant-in-Aid for Scientific
Research (Project Number: 25289118), a JSPS Grand-in-Aid for Scientific Research (Project Number: 18H03204)
## Documentation
Each file is documented in its header.
Changes are (lightly) documented in [changelog.txt](changelog.txt).
## Installation with Windows 10 & 11
Installation of infotheo on Windows is less simple.
See [this page](https://github.com/affeldt-aist/mathcomp-install/blob/master/install-windows-en.org)
for instructions to install MathComp on Windows 10 & 11
(or [this page](https://staff.aist.go.jp/reynald.affeldt/ssrcoq/install.html) for instructions in Japanese).
Once MathComp is installed (with opam), do
`opam install coq-infotheo` or `git clone git@github.com:affeldt-aist/infotheo.git; opam install .`
## Original License
Before version 0.2, infotheo was distributed under the terms of the
`GPL-3.0-or-later` license.