Projects
These are some of the projects I have worked on.Kleenex
Kleenex is a domain-specific programming language for specifying high-performance streaming string processing programs. Its semantics is based on non-deterministic finite state transducers, a generalization of finite-state automata commonly known as the machine model for regular expressions.
BoxProver
BoxProver is a web-based proof assistant for teaching the formal proof theory of first-order logic. It has been used as such in the BSc course "Logic in Computer Science" at DIKU. Students may enter their proofs in a textual format and have them verified by BoxProver, which then typesets the finished proofs using Fitch-style natural deduction. The notation used in the rendered proofs closely matches that of Huth and Ryan's textbook Logic in Computer Science, and thus requires a minimal amount of mental effort converting between notations.
The Twelf proof assistant is used internally for checking that proofs are valid with respect to a formalization of Fitch-style natural deduction in the LF logical framework. Twelf is used purely as a type checker for LF, however, and BoxProver uses none of its meta-logical reasoning facilities.