2015FURNISSAEPhD.pdf (704.7 kB)
HybridLF: a system for reasoning in higher-order abstract syntax
thesis
posted on 2015-10-22, 15:25 authored by Amy Elizabeth FurnissIn this thesis we describe two new systems for reasoning about deductive
systems: HybridLF and Canonical HybridLF.
HybridLF brings together the Hybrid approach (due to Ambler, Crole
and Momigliano [15]) to higher-order abstract syntax (HOAS) in Isabelle/HOL
with the logical framework LF, a dependently-typed system for proving theorems
about logical systems. Hybrid provides a version of HOAS in the form of
the lambda calculus, in which Isabelle functions are automatically converted
to a nameless de Bruijn represenation. Hybrid allows untyped expressions to
be entered as human-readable functions, which are then translated into the
machine-friendly de Bruijn form. HybridLF uses and updates these techniques
for variable representation in the context of the dependent type theory
LF, providing a version of HOAS in the form of LF.
Canonical HybridLF unites the variable representation techniques of
Hybrid with Canonical LF, in which all terms are in canonical form and definitional
equality is reduced to syntactic equality. We extend the Hybrid approach
to HOAS to functions with multiple variables by introducing a family
of abstraction functions, and use the Isabelle option type to denote errors instead
of including an ERR element in the Canonical HybridLF expression
type.
In both systems we employ the meta-logic M2 to prove theorems about
deductive systems. M2 [28] is a first-order logic in which quantifiers range
over the objects and types generated by an LF signature (that encodes a
deductive system). As part of the implementation of M2 we explore higher-order
unification in LF, adapting existing approaches to work in our setting.
History
Supervisor(s)
Crole, Roy; Ridge, ThomasDate of award
2015-10-20Author affiliation
Department of Computer ScienceAwarding institution
University of LeicesterQualification level
- Doctoral
Qualification name
- PhD