changeme
This commit is contained in:
parent
a8189d75a7
commit
9ccd292dfe
1 changed files with 11 additions and 9 deletions
20
About
20
About
|
@ -89,18 +89,20 @@ Her Erdős number is 4.
|
||||||
|
|
||||||
#### Hannes
|
#### Hannes
|
||||||
|
|
||||||
Hannes is a research associate at the University of Cambridge. He enjoys to write
|
Hannes enjoys living in Berlin, Germany. Until end of 2017, he used to be a research
|
||||||
code, and also travelling and repairing his recumbent bicycle, and being a
|
associate at the University of Cambridge in the [rems](https://rems.io) project.
|
||||||
barista.
|
He enjoys to write code, and also travelling and repairing his recumbent
|
||||||
|
bicycle, and being a barista.
|
||||||
|
|
||||||
Hannes did his PhD in computer science about formal verification of
|
Hannes did his PhD in computer science about [formal verification of imperative
|
||||||
imperative code (using a higher-order separation logic and the theorem prover
|
code](https://itu.dk/research/tomeso/) (using a higher-order separation logic
|
||||||
Coq). At the moment he is working on an executable formal model of
|
and the theorem prover Coq). Hannes co-authored [not-quite-so-broken
|
||||||
|
TLS](https://nqsb.io), a TLS implementation from the grounds up in OCaml, and
|
||||||
|
contributes to the MirageOS project as a core team member. He is working on
|
||||||
|
various projects, including opam signing and
|
||||||
|
[netsem](https://www.cl.cam.ac.uk/~pes20/Netsem/), an executable formal model of
|
||||||
TCP/IP which can act as a test validator.
|
TCP/IP which can act as a test validator.
|
||||||
|
|
||||||
Hannes co-authored a TLS implementation from the grounds up in OCaml, and
|
|
||||||
contributes to the MirageOS project as a core team member.
|
|
||||||
|
|
||||||
#### Paul
|
#### Paul
|
||||||
|
|
||||||
Paul is an independent IT consultant located in Copenhagen.
|
Paul is an independent IT consultant located in Copenhagen.
|
||||||
|
|
Loading…
Reference in a new issue