Hans de Nivelle
- Hans de Nivelle received his PhD from Delft University of Technology in 1995. Title was ‘Ordering Refinements of Resolution’
- From 1996 until 1999, he worked at University of Amsterdam and Centrum voor Wiskunde en Informatica, the Netherlands.
- From 1999 until 2007, he worked at Max-Planck Institute for Computer Science in Saarbruecken, Germany
- From 2007 until 2017, he was professor at University of Wroclaw, Poland
I am interested in automated theorem proving, verification of mathematical proofs, and programming language design. Before and shortly after I came to Nazarbayev University, I worked on a new calculus for automated theorem proving in first-order logic. I have delayed this research for the time being because it is too specialized.
Since the beginning of 2020, I work on a new programming language which is aimed at the implementation of logic. After having tried many programming languages for my theorem provers, I concluded that not one of them is suitable for implementation of logic. I starting designing and implementing a programming language that is strongly typed with a type system that is flexible enough to accept the complicated recursive structure of logical formulas without need for additional casting. In order to obtain this, one needs adaptive typing, which means that data refine their types dependent on context. We expect the language to be nice, efficient and usable in other areas as well. This research is supported by grant ‘Designing and Implementing a Programming Language for Logic’ (021220FD1651).
I am involved in teaching Performance and Datastructures (CSCI 152), Programming Languages (CSCI 235), Formal Languages (CSCI 272), and Compiler Construction (CSCI 355).
I am a member of the TABLEAUX Steering Committee. I frequently participate in PCs of international conferences.