summaryrefslogtreecommitdiffstats
path: root/content/zettel/3a9.md
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2023-05-11 19:38:03 +0100
committerYann Herklotz <git@yannherklotz.com>2023-05-11 19:38:03 +0100
commit47c1289ff658a5aec71635d79ffe30bb29a07876 (patch)
tree56cf6b959e37fed88c492d34defd3d7ec40e7148 /content/zettel/3a9.md
parentfbe0fc62120348f582dc4db2b614078943d0764b (diff)
downloadzk-web-47c1289ff658a5aec71635d79ffe30bb29a07876.tar.gz
zk-web-47c1289ff658a5aec71635d79ffe30bb29a07876.zip
Add content
Diffstat (limited to 'content/zettel/3a9.md')
-rw-r--r--content/zettel/3a9.md24
1 files changed, 24 insertions, 0 deletions
diff --git a/content/zettel/3a9.md b/content/zettel/3a9.md
new file mode 100644
index 0000000..936da67
--- /dev/null
+++ b/content/zettel/3a9.md
@@ -0,0 +1,24 @@
++++
+title = "Teams working on CompCert"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3a8"]
+forwardlinks = ["3a8", "3a10"]
+zettelid = "3a9"
++++
+
+[Verimag]
+: Works on CompCert-KVX, Hash consing in CompCert, Impure computations
+ in Coq.
+
+[Celtique]
+: Works on constant time CompCert and CompCertSSA ([\#3a8]).
+
+[Xavier Leroy]
+: Works on original CompCert.
+
+ [Verimag]: https://www-verimag.imag.fr/FormalProofs-members.html
+ [Celtique]: https://team.inria.fr/celtique/
+ [\#3a8]: /zettel/3a8
+ [Xavier Leroy]: https://xavierleroy.com/