The University of Kent, Canterbury, Kent, CT2 7NZ, T +44 (0)1227 764000
Ms Jael Kriener
Corrigendum: There is a mathematical error in "RedAlert: Determinacy Inferende for Prolog" -- I'm working on fixing it.
Proving Equivalences Between Prolog Semantics in Coq -- companion webpage to "Proofs you can believe in" (PPDP 2013), including Coq scripts and html versions of sources.
mux -- demo-version of the mux-algorithm described in "Mutual Exclusion by Interpolation" (FLOPS 2012)
You can find a report on an implementation of a cut-free sequent calculus for logics with adjoint modalities I did under the supervision of Roy Dyckhoff here.
And if you're really keen, you can have a look at either one of my two BSc-dissertations here:
Puzzle Design using Constraint Programming
Joseph Butler on Self-Deceit and Hypocrisy
PhD Project Summary
I am supervised by Andy King.
The focus of my work lies on provably correct static analyses of declarative programs, in particular on determinacy analyses. I have been working on determinacy inference (i.e. inferring deterministic modes) for logic programs containing cut.
I am a member of the following research groups:
Aside from my (obvious) interest in my PhD project, I am interested in:
- Static Analysis more generally,
- SAT, SMT and Constraint Modelling and Solving,
- All Things Logical: Formal and Automated Reasoning of all sorts, particularly Automated and Interactive Theorem Proving, again particularly Coq, Proof Theory, Non-Classical Logics, History of Logic, etc
TeachingI am not teaching this semester.
But that doesn't mean you can't come and ask me questions! If you're a student with us and you feel like talking about logic/ functional programming/ maths/ etc... come by my office!
I have previously taught on the following:
CO322: Foundations of Computing
CO537: Functional Programming
CO841: Contracts, Professional Responsibility & Computer Law
CO844: Logic and Logic Programming