基本信息
浏览量:44
职业迁徙
个人简介
I'm a mathematician (without a specialization, but with a fondness for algebraic and topological subjects), who tried to learn physics (and failed) and computers (love them, but only when they're not a mess.) My M.Sc. thesis was about the geometry of supergravity (that's mathematical physics) and my Ph.D. thesis was about conservativity in modular specifications (that's mathematical computer science.) After I got my Ph.D. I worked for six years as a system and network administrator at Utrecht University. I'm currently working in the project of Henk Barendregt. I used to be a Coq programmer in the fundamental theorem of algebra project, and then I was a four-year postdoc. Currently I've become an assistant professor and at the moment I'm teaching a course about proof assistants for master's students. I also am tutor of a few students. Finally I keep a weblog with interviews of our students (as propaganda for our study).
I don't have too many publications of my own (one of them is a comparison between provers), but I wrote several notes and I sometimes give talks. I authored one computer program: an Automath checker. It's portable (vanilla C), simple (3000 lines of code) and fast (on my current computer the test file which is Jutting's translation of a complete mathematical book gets checked in 0.6 seconds.) A simpler thing I authored is a small script called raft for doing proof developments with Otter. Something else I did: I compiled a list of computer math systems to investigate the state of the art in digital mathematics, which I have put on the web and will try to keep complete and up to date. And I wrote a small page about Mizar, which is a system for proof checking that deserves to be known much better than it is. I also wrote a page with a list of possible proof checking projects. And then I have a page which investigated which of a list of 100 theorems have been formalized in which systems. Finally, I organised a session with proof assistant demos at ICMS 2006.
研究兴趣
论文共 102 篇作者统计合作学者相似作者
按年份排序按引用量排序主题筛选期刊级别筛选合作者筛选合作机构筛选
时间
引用量
主题
期刊级别
合作者
合作机构
Aaron Ballman, Alex Gilding,Jens Gustedt, Thomas R. W. Scogland,Robert C. Seacord,Martin Uecker,Freek Wiedijk
HAL (Le Centre pour la Communication Scientifique Directe) (2020)
引用0浏览0引用
0
0
Annals of Mathematics and Artificial Intelligenceno. 2-4 (2019): 213-257
CoRR (2019)
引用0浏览0EI引用
0
0
Computational Logic (2014)
引用41浏览0EI引用
41
0
加载更多
作者统计
合作学者
合作机构
D-Core
- 合作者
- 学生
- 导师
数据免责声明
页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果,我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问,可以通过电子邮件方式联系我们:report@aminer.cn