Skip to content

Commit

Permalink
README.md: add user
Browse files Browse the repository at this point in the history
  • Loading branch information
fblanqui committed Jan 10, 2025
1 parent 1289df2 commit ccfa0e7
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ Some users
- [Alessio Coltellacci](https://github.com/NotBad4U) and [Stephan Merz](https://members.loria.fr/Stephan.Merz/): encoding of TLA+ set theory in Lambdapi [[ABZ'23]](https://doi.org/10.1007/978-3-031-33163-3_29)
- [Jean-Paul Bodeveix](https://www.irit.fr/~Jean-Paul.Bodeveix/) and Anne Grieu: certification of Event-B proofs generated by Rodin in Lambdapi
- [Frédéric Blanqui](https://blanqui.gitlabpages.inria.fr/): translation of HOL-Light proofs to Coq [[github]](https://github.com/Deducteam/hol2dk) [[LPAR'24]](https://doi.org/10.29007/6k4x)
- Nicolas Margulies: a formalization of cubical type theory in Lambdapi [[github]](https://github.com/nicomarg/CubicalDk)
- [Thomas Traversié](https://thomastraversie.github.io/): implementation of set theory with pointed graphs [[LFMTP'22]](https://hal.inria.fr/hal-03740004)
- [Quentin Garchery](https://www.lri.fr/~garchery/): certification of Why3 proof task transformations in Lambdapi [[PhD thesis]](https://inria.hal.science/tel-03560564)
- Gabriel Hondet: translation of PVS statements to Lambdapi [[github]](https://github.com/Deducteam/personoj) [[PhD thesis]](https://inria.hal.science/tel-03855351)
Expand Down

0 comments on commit ccfa0e7

Please sign in to comment.