-
Notifications
You must be signed in to change notification settings - Fork 0
/
index.html
228 lines (195 loc) · 11.8 KB
/
index.html
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
227
228
<!DOCTYPE html>
<html lang="en-US">
<head>
<title>The red* family of proof assistants</title>
<meta charset="utf-8" />
<meta name="viewport" content="width=device-width, initial-scale=1" />
<link rel="stylesheet" href="https://unpkg.com/[email protected]/build/pure-min.css" integrity="sha384-cg6SkqEOCV1NbJoCu11+bm0NvBRc8IYLRGXkmNrqUBfTjmMYwNKPWBTIKyw9mHNJ" crossorigin="anonymous">
<link rel ="stylesheet" href="https://fonts.googleapis.com/css2?family=Roboto:wght@400;500&display=swap">
<link rel="stylesheet" href="https://unpkg.com/[email protected]/build/grids-responsive-min.css">
<link rel="stylesheet" href="style.css" />
</head>
<body>
<div class="wrapper">
<h1>The <span class="revolutionary">red</span>* family of proof assistants</h1>
<div class="pure-g" id="boxes">
<div class="pure-u-2-3 pure-u-md-1-5 box">
<a href="#algae">
<h2><span class="algae">A.L.G.A.E.</span></h2>
<p>A collection of libraries for developing proof assistants.</p>
</a>
</div>
<div class="pure-u-2-3 pure-u-md-1-5 box">
<a href="#cooltt">
<h2><span class="cool">cool</span>tt</h2>
<p>A prototype proof assistant for Cartesian cubical type theory.</p>
</a>
</div>
<div class="pure-u-2-3 pure-u-md-1-5 box">
<a href="#redtt">
<h2><span class="revolutionary">red</span>tt</h2>
<p>A proof assistant for Cartesian cubical type theory.</p>
</a>
</div>
<div class="pure-u-2-3 pure-u-md-1-5 box">
<a href="#redprl">
<h2><span class="revolutionary">Red</span>PRL</h2>
<p>A Nuprl-style proof assistant for computational Cartesian cubical type theory.</p>
</a>
</div>
</div> <!-- /.pure-g -->
<div class="content">
<p>
The core <span class="revolutionary">Red</span><b>PRL</b> Development Team
(<a href="https://www.cs.cmu.edu/~cangiuli/">Carlo Angiuli</a>,
<a href="https://www.cs.cmu.edu/~ecavallo/">Evan Cavallo</a>,
<a href="https://favonia.org/">Kuen-Bang Hou (Favonia)</a>,
<a href="https://totbwf.github.io">Reed Mullanix</a>,
and <a href="http://www.jonmsterling.com/">Jon Sterling</a>) has
developed several experimental proof assistants for Cartesian cubical
type theory with the collaboration of
<a href="https://www.cs.cmu.edu/~rwh/">Robert Harper</a>. We are also building
generic components and tools for modularly implementing proof assistants and elaborators.
</p>
<div class="pure-g">
<div class="pure-u-1 pure-u-lg-3-5 left-box">
<h2 id="algae">The <span class="package-name"><span class="algae">A.L.G.A.E.</span></span> Project</h2>
<p>
We are developing composable (OCaml) libraries that facilitate the construction of a usable proof assistant from a core type checker.
Currently, we are exploring the use of <span class="algae">algebraic effects</span> (instead of monads) to structure our libraries.
So far, we have built these libraries specific to proof assistants:
</p>
<ul>
<li>🩺 <a href="https://github.com/RedPRL/asai"><span class="package-name">asai</span></a>: compiler diagnostics</li>
<li>📚 <a href="https://github.com/RedPRL/bantorra"><span class="package-name">bantorra</span></a>: library management</li>
<li>♾️ <a href="https://github.com/RedPRL/mugen"><span class="package-name">mugen</span></a>: universe levels</li>
<li>📚 <a href="https://github.com/RedPRL/kado"><span class="package-name">kado</span></a>: cofibrations in Cartesian cubical type theory</li>
<li>👹 <a href="https://github.com/RedPRL/yuujinchou"><span class="package-name">yuujinchou</span></a>: hierarchical names and lexical scoping</li>
</ul>
<p>
We also have a few libraries for general purposes:
</p>
<ul>
<li>🦠 <a href="https://github.com/RedPRL/algaeff"><span class="package-name"><span class="algae">algae</span>ff</span></a>: composable effects-based components</li>
<li>🔙 <a href="https://github.com/RedPRL/ocaml-bwd"><span class="package-name">bwd</span></a>: backward lists</li>
</ul>
We have a prototype <a href="https://github.com/redprl/algaett"><span class="package-name"><span class="algae">algae</span>tt</span></a> (in progress) that demonstrates how to build a usable system using these libraries.
<h3>Publications and talks</h3>
<ul>
<li>Gratzer, S, A, Coquand, Birkedal. <a href="https://arxiv.org/abs/2210.05420">Controlling unfolding in type theory</a>.</li>
<li>F, A, M. <a href="https://doi.org/10.1145/3571250">An Order-Theoretic Analysis of Universe Polymorphism</a>. <em>POPL 2023</em>.</li>
<li>F. <a href="https://youtu.be/5Cp8jNrWSjI">A Domain-Specific Language for Name Modifiers</a>. <em>TYPES 2022</em>.</li>
</ul>
</div>
</div>
<div class="pure-g">
<div class="pure-u-1 pure-u-lg-3-5 left-box">
<h2 id="cooltt">The <span class="package-name"><span class="cool">cool</span>tt</span> proof assistant</h2>
<p>
We are currently developing <span class="package-name"><span class="cool">cool</span>tt</span>, a prototype proof assistant for Cartesian
cubical type theory, building on our previous work on the
<span class="package-name"><span class="revolutionary">red</span>tt</span> proof assistant.
<span class="package-name"><span class="cool">cool</span>tt</span> supports <em>systems</em> for eliminating disjunctions
of cofibrations, implementing the full definitional η-law.
</p>
<ul>
<li><a href="https://github.com/redprl/cooltt">Source on GitHub</a></li>
<li><a href="https://redprl.github.io/cooltt/cooltt/">Internal documentation</a></li>
</ul>
<h3>Publications and talks</h3>
<ul>
<li>
S. <a href="https://www.jonmsterling.com/sterling-2022-wits.xml">Make Three To Throw Away: Frontiers in Homotopical Proof Assistants</a>. <em>Workshop on the Implementation of Type Systems</em> (keynote).
</li>
</ul>
<p>
We welcome new contributors!
</p>
</div>
<div class="pure-u-1 pure-u-lg-2-5 right-box">
<img class="pure-img" alt="Screenshot of cooltt." src="img/cooltt-screenshot.png" />
</div>
</div>
<div class="pure-g">
<div class="pure-u-1 pure-u-lg-3-5 left-box">
<h2 id="redtt">The <span class="package-name"><span class="revolutionary">red</span>tt</span> proof assistant</h2>
<p>
A proof assistant for Cartesian cubical type theory. Notable features include extension types,
user-defined (parametric) higher inductive types, and rudimentary higher-order unification;
<span class="package-name"><span class="revolutionary">red</span>tt</span> pioneered the
<em>boundary-sensitive</em> treatment of holes that now appears in
<a href="https://agda.readthedocs.io/en/latest/language/cubical.html">Cubical Agda</a> and
<span class="package-name"><span class="cool">cool</span>tt</span>.</p>
<ul>
<li><a href="https://github.com/redprl/redtt">Source on GitHub</a></li>
<li><a href="https://github.com/RedPRL/redtt/tree/master/library">The
<span class="package-name"><span class="revolutionary">red</span>tt</span>
mathematical library</a></li>
</ul>
<h3>Publications and talks</h3>
<ul>
<li>
S. <a href="http://math.andrej.com/2020/06/01/redtt-and-the-future-of-cartesian-cubical-type-theory/"><span class="package-name"><span class="revolutionary">red</span>tt</span> and the future of Cartesian cubical type theory</a>.
<em>Every proof assistant</em> seminar.
</li>
<li>
F. <a href="https://youtu.be/9pc4QkMtrnQ">Towards Efficient Cubical Type Theory</a>.
<em>Homotopy Type Theory Electronic Seminar Talks (HOTTEST)</em>.
</li>
<li>
A, C, F, H, Mörtberg, S. <a href="http://www.jonmsterling.com/pdfs/dagstuhl.pdf"><span class="package-name"><span class="revolutionary">red</span>tt</span>: implementing Cartesian cubical type theory</a>.
<em>Dagstuhl Seminar 18341: Formalization of Mathematics in Type Theory</em>.
</li>
</ul>
</div>
<div class="pure-u-1 pure-u-lg-2-5 right-box">
<img class="pure-img" alt="Screenshot of redtt." src="img/redtt-screenshot.png" />
</div>
</div>
<div class="pure-g">
<div class="pure-u-1 pure-u-lg-3-5 left-box">
<h2 id="redprl">The <span class="revolutionary">Red</span>PRL proof assistant</h2>
<p>
A tactic-based proof assistant for computational Cartesian cubical type theory inspired by
<a href="http://www.nuprl.org">Nuprl</a>.
<span class="package-name"><span class="revolutionary">Red</span>PRL</span> implements a two-level cubical
type theory which includes univalent universes, some higher inductive types, and strict
equality types with equality reflection.
</p>
<ul>
<li><a href="https://redprl.readthedocs.io/en/latest/">Documentation on Read the Docs</a></li>
<li><a href="https://github.com/redprl/sml-redprl">Source on GitHub</a></li>
<li><a href="https://github.com/RedPRL/sml-redprl/blob/master/CONTRIBUTORS.md">Full list of
contributors</a></li>
</ul>
<h3>Publications and talks</h3>
<ul>
<li>
A, C, F, H, S. <a href="http://eptcs.web.cse.unsw.edu.au/paper.cgi?LFMTP2018.1">The <span class="package-name"><span class="revolutionary">Red</span>PRL</span> Proof Assistant</a>. LFMTP 2018.
</li>
<li>
A, H. <a href="https://popl18.sigplan.org/track/POPL-2018-TutorialFest">Computational Higher Type Theory</a>. Tutorial at POPL 2018.
</li>
</ul>
</div>
<div class="pure-u-1 pure-u-lg-2-5 right-box">
<img class="pure-img" alt="Screenshot of RedPRL." src="img/redprl-screenshot.png" />
</div>
</div>
<h2>Acknowledgments</h2>
<p>
This research was sponsored by the Air Force Office of Scientific Research under grant
number FA9550-15-1-0053 and the National Science Foundation under grant number DMS-1638352.
We thank the Logic and Semantics Group at Aarhus University for their hospitality in during
the summer of 2018, during which part of this work was undertaken. We also thank the Isaac
Newton Institute for Mathematical Sciences for its support and hospitality during the
program "Big Proof" when part of this work was undertaken; the program was supported by the
Engineering and Physical Sciences Research Council under grant number EP/K032208/1. The
views and conclusions contained here are those of the authors and should not be interpreted
as representing the official policies, either expressed or implied, of any sponsoring
institution, government or any other entity.
</p>
</div> <!-- /.content -->
</div> <!-- /.wrapper -->
</body>
</html>