Please use this identifier to cite or link to this item: http://hdl.handle.net/2381/33362
Title: HybridLF: a system for reasoning in higher-order abstract syntax
Authors: Furniss, Amy Elizabeth
Supervisors: Crole, Roy
Ridge, Thomas
Award date: 20-Oct-2015
Presented at: University of Leicester
Abstract: In 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.
Links: http://hdl.handle.net/2381/33362
Type: Thesis
Level: Doctoral
Qualification: PhD
Rights: Copyright © the author. All rights reserved.
Appears in Collections:Leicester Theses
Theses, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
2015FURNISSAEPhD.pdf704.7 kBAdobe PDFView/Open


Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.