- Homepage
- About the Joint Centre
- Research Areas & Projects
- Researchers
- News & Events
- Open Positions
Bld I, Microsoft Research-INRIA Joint Centre
Two encounters with Coq: dependently typed regular expressions and handshaking with a computer algebra system
Vladimir Komendantsky
School of Computer Sciences,
St Andrews University
In this short introduction I’m going to first talk about my recent industrial consultancy experience and present a dependent type of regular expressions and explain its relevance to non-deterministic finite automata (therefore turning the page on an unfinished 90’s Coq contribution by J.-C. Filliatre) and its cumbersomeness for quotient constructions on regular expressions such as partial derivatives (V. Antimirov; 1995). I will also present results of a 3-month mini-project on communication between Coq and the computer algebra system GAP that has recently finished in the University of St Andrews (but is likely to continue in a less formal mode).