I haven't had much to say recently. I rather doubt anyone has noticed, and yet nevertheless I feel a bit guilty... Perhaps this indicates some underlying psychological problem? Anyway, I have an excuse: I was working on two different papers with various colleagues. If things work out I may infinitely increase my publication list!
The first, entitled Focused Inductive Theorem Proving describes the theory behind our interactive and automatic theorem prover for an intuitionist logic with support for generic quantification (using nabla, which is nice for reasoning about systems with names and binding) and definitions (via fixed points, which are useful for encoding inductive and coinductive data structures, like lists and streams, respectively). The system is called Tac, and is released under the GPL version 3. One fun note: we have (kind of, call it mostly) solved the POPLMark challenge parts 1A and 2A with Tac.
The second is A Meta-Programming Approach to Realizing Dependently Typed Logic Programming, and describes a technique that we developed to implement logic programming in LF via translation to λProlog, a higher order logic programming with an efficient bytecode based implementation. The tool, named Parinati, is also available under the GPL version 3.
Other than that I've been snowboarding and working on a fun little side project, which will be to topic of my next update, which I am sure you eagerly await.
No comments:
Post a Comment