Publications
122 results found
Gardner P, 1994, Discovering needed reductions using type theory, Pages: 555-574, ISSN: 0302-9743
The identification of the needed redexes in a term is an un decidable problem. We introduce a (partially decidable) type assignment system, which distinguishes certain redexes called the allowable redexes. For a well-typed term e, allowable redexes are-needed redexes. In addition, with principal typing, all the needed redexes of a normalisable term are allowable. Using these results, we are able to identify all the needed reductions of a principally typed normalisable term. Possible applications of these results include strictness and sharing analysis for functional programming languages, and a reduction strategy for well-typed terms which satisfies Lévy’s notion of optimal reduction.
Gardner P, 1993, A new type theory for representing logics, Pages: 146-157, ISSN: 0302-9743
We propose a new type theory for representing logics, called LF+ and based on the Edinburgh Logical Framework. The new framework allows us to give, apparently for the first time, general definitions which capture how well a logic has been represented. Using our definitions, we show that, for example, first-order logic can be well-represented in LF+, whereas linear and relevant logics cannot. These syntactic definitions of representation have a simple formulation as indexed isomorphisms, which both confirms that our approach is a natural one, and provides a link between type-theoretic and categorical approaches to frameworks.
This data is extracted from the Web of Science and reproduced under a licence from Thomson Reuters. You may not copy or re-distribute this data in whole or in part without the written consent of the Science business of Thomson Reuters.