palmskog/README.md
About me
I am a researcher and teacher at KTH Royal Institute of Technology in the Department of Theoretical Computer Science and the STEP research group. I do research primarily on topics related to program verification and proof engineering.
Research interests
I am interested in development of techniques and tools based on proof assistants for construction of functionally correct and secure software systems; see my research publications on DBLP and Google Scholar. I use Rocq for both proving and programming and am a member of the Rocq Team, where I help maintain the Rocq opam archive, the Rocq Platform, and Rocq-community. I also use HOL4 and usually program in languages in the ML family such as OCaml, Standard ML, and CakeML.
Pinned Loading
-
kth-step/mil kth-step/mil Public
Formal definition, metatheory, and tools for the Machine Independent Language using HOL4 and CakeML
Standard ML 2
-
rocq-community/reglang rocq-community/reglang Public
Regular Language Representations in Coq [maintainers=@chdoc,@palmskog]
-
rocq-community/aac-tactics rocq-community/aac-tactics Public
Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainer=@palmskog]