Papers by M Hofmann on HOAS & on Linear Types
Subject: Papers by M Hofmann on HOAS & on Linear Types
From: "Martin Hofmann" <email@example.com>
Date: Fri, 30 Apr 1999 11:34:29 +0100 (BST)
In-reply-to: <199904300156.VAA14597@saul.cis.upenn.edu> (firstname.lastname@example.org)
I would like to draw your attention to the final versions of two
papers of mine which will be presented at LICS '99 in Trento. Comments
are very welcome!
Paper1: Linear types and non-size-increasing polynomial time computation.
We propose a linear type system with recursion operators for inductive
datatypes which ensures that all definable functions are polynomial
time computable. The system improves upon previous such systems in
that recursive definitions can be arbitrarily nested, in particular no
predicativity or modality restrictions are made.
While you're at it you might also wish to take a look at my recently
finished "habilitation thesis" in http://www.dcs.ed.ac.uk/home/mxh/habil.ps.gz
Paper2: Semantical analysis of higher-order abstract syntax
Synopsis: A functor category semantics for higher-order abstract syntax is
proposed with the following aims: relating higher-order and first
order syntax, justifying induction principles, suggesting new logical
principles to reason about higher-order syntax.