[Prev][Next][Index][Thread]

Papers by M Hofmann on HOAS & on Linear Types


Dear all,

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.

Synopsis: 
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. 

Source: http://www.dcs.ed.ac.uk/home/mxh/lics99icfp.ps.gz

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. 

Source: http://www.dcs.ed.ac.uk/home/mxh/lics99hoas.ps.gz

Best wishes,
 Martin Hofmann