Faré
2018-07-30 22:15:10 UTC
Dear Coq-Clubbers,
Legicash, the startup I co-founded earlier this year in Boston, MA to
develop smart contracts using formal methods, has found some early
investors. We're looking to expand our team. We have several positions
ranging from junior developer to senior manager, and we are looking
for people with interest and if possible experience in using formal
methods in general and Coq in particular. We prefer our coworkers to
be living in the Boston area or ready to move here, but we will
consider remote applicants if you are experienced.
We described our general approach in several posts on
https://medium.com/legi — we also have more technical documents and
source code that we intend to opensource eventually, but are willing
to share with interested people already.
We currently have a demo written in OCaml, and are considering porting
it all to Coq (from which OCaml code would be extracted, and more),
after it reaches its next milestone. We are especially interested in
help from people with experience in building applications as extracted
from a Coq specification, or in using reflection to reason based on an
internal model of some other logic embedded in Coq.
We have also started a research group called Belvedere to build the
fundamental infrastructure for smart contracts based on our high-level
point of view. Pierre-Yves Strub, Matthieu Sozeau and Nada Amin have
already joined this group.
We are looking for at least one additional member who would join us
and be able to supervise a PhD thesis. We as a group are currently
working on a funding proposal from the Tezos Foundation, but are also
looking on other potential sources of funding (including by Legicash
directly if we otherwise find sufficient funding).
If you are a Coq user novice or experienced, or a researcher with a
strong interest in using Coq to work on distributed applications,
please contact us. We intend to simultaneously advance science and
have an impact on real-world applications, one by the other.
—♯ƒ • François-René ÐVB Rideau •Reflection&Cybernethics• http://fare.tunes.org
There are two hard things in computer science: cache invalidation,
naming things, and off-by-one errors.
Legicash, the startup I co-founded earlier this year in Boston, MA to
develop smart contracts using formal methods, has found some early
investors. We're looking to expand our team. We have several positions
ranging from junior developer to senior manager, and we are looking
for people with interest and if possible experience in using formal
methods in general and Coq in particular. We prefer our coworkers to
be living in the Boston area or ready to move here, but we will
consider remote applicants if you are experienced.
We described our general approach in several posts on
https://medium.com/legi — we also have more technical documents and
source code that we intend to opensource eventually, but are willing
to share with interested people already.
We currently have a demo written in OCaml, and are considering porting
it all to Coq (from which OCaml code would be extracted, and more),
after it reaches its next milestone. We are especially interested in
help from people with experience in building applications as extracted
from a Coq specification, or in using reflection to reason based on an
internal model of some other logic embedded in Coq.
We have also started a research group called Belvedere to build the
fundamental infrastructure for smart contracts based on our high-level
point of view. Pierre-Yves Strub, Matthieu Sozeau and Nada Amin have
already joined this group.
We are looking for at least one additional member who would join us
and be able to supervise a PhD thesis. We as a group are currently
working on a funding proposal from the Tezos Foundation, but are also
looking on other potential sources of funding (including by Legicash
directly if we otherwise find sufficient funding).
If you are a Coq user novice or experienced, or a researcher with a
strong interest in using Coq to work on distributed applications,
please contact us. We intend to simultaneously advance science and
have an impact on real-world applications, one by the other.
—♯ƒ • François-René ÐVB Rideau •Reflection&Cybernethics• http://fare.tunes.org
There are two hard things in computer science: cache invalidation,
naming things, and off-by-one errors.