The chip from palmskog

chip's Introduction

About me

I am a researcher and teacher at KTH Royal Institute of Technology in the Theoretical Computer Science division 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 Coq for both proving and programming and am a member of the Coq Team, where I help maintain the Coq opam archive, the Coq Platform, and Coq-community. I also use HOL4 and usually program in languages in the ML family such as OCaml, Standard ML, and CakeML.

chip's People

Contributors

Stargazers

Watchers

chip's Issues

Port to the latest version of `mathcomp`

I was looking for the implementation of topological sorting in Coq (in particular I need it to prove that any finite partial order can be extended to a total order).
@palmskog kindly pointed me to this library, and this lemma, which provides exactly what I need.

However, the problem is that currently I use some features from the dev version of mathcomp, but chip requires mathcomp.1.7

Therefore, it would be really great to update chip to the latest version of mathcomp.

Recommend Projects