Mechanising Aspects of MiniKanren
Ramana Kumar (ANU)
LOGIC AND COMPUTATION SEMINARDATE: 2010-06-18
TIME: 12:00:00 - 13:00:00
LOCATION: RSISE Video Conference Room (A207)
CONTACT: JavaScript must be enabled to display this email address.
ABSTRACT:
miniKanren is an embedding of Logic Programming in Scheme. This talk presents the PhB Honours thesis of the speaker and reports on his achievements in proving termination and correctness of unification algorithms for first-order and nominal terms. He also gives a formal semantics of miniKanren and proves a soundness result for the denotational and operational forms. All the work was verified using the HOL4 proof assistant.
BIO:
Ramana Kumar is finishing his PhB (Hons) program at ANU. His thesis supervisor is Michael Norrish.
