Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 John Hughes
I introduced a course in Advanced
Functional Programming, to teach senior
undergraduates to solve substantial problems in Haskell.
Course topics include lazy evaluation, design of
combinator libraries, parsing and pretty-printing, monads
and continuations. The course is taught in a `problem
based' manner.
I have prepared a one week intensive course for doctoral
students on Program Specialisation,
which has been given here at Chalmers University and at
the University of Montevideo.
Combining Verification Methods in Software Development (Cover).
Flexible System-on-Chip Platforms for Embedded Applications (FlexSoC).
The documents contained in these directories are
included by the contributing authors as a means to ensure timely
dissemination of scholarly and technical work on a non-commercial
basis. Copyright and all rights therein are maintained by the
authors or by other copyright holders, notwithstanding that they
have offered their works here electronically. It is understood
that all persons copying this information will adhere to the
terms and constraints invoked by each author's copyright. These
works may not be reposted without the explicit permission of the
copyright holder.
My research interests are functional programming in general,
and program analysis and transformation in particular.
Type Specialisation
for the Lambda-calculus; or, A New Paradigm for
Partial Evaluation based on Type Inference,
presented at the Dagstuhl
Seminar on Partial Evaluation. Describes a
partial evaluator which specialises not only
expressions, but types. So a universal type in an
interpreter, for example, may be specialised to
arbitrary types in the residual versions. This
leads to optimal specialisation, that is,
complete removal of a layer of interpretation ---
the first time this has been achieved for a typed
higher-order language. Other interesting results
include the combination of constructor
specialisation with higher-order functions,
leading to `firstification for free'.
While
previous partial evaluators have been, in a
sense, generalised evaluators, this one is a
generalised type-checker --- hence the `new
paradigm'.
In addition to the full paper, there is a Glasgow workshop
paper that gives an informal introduction to
the basic ideas. (bibtex).
A type
specialisation tutorial was presented at the
DIKU Summer School on Partial Evaluation. This
article also describes a new type-based arity
raiser used as a post-processor, and shows new
applications of type specialisation to
transforming polymorphic programs to monomorphic
ones, and modelling constructor specialisation by
polyvariance. The examples in the paper can be
run on the online
demo.
I spoke about type specialisation as a Strachey
Lecture in Oxford.
There is a demo
of the partial evaluator available. You can if
you wish get the sources.
There is also a new version
of the type specialiser available, which is nicer
to use thanks to some syntactic sugar, and which
includes a type-based arity raiser.
Per Sjörs has implemented a type specialiser for
a subset of Haskell, as his Masters project (Masters thesis,
abstract).
Arrows
I've also been working on `arrows', an alternative to
monads for structuring combinator libraries. I gave a
talk on the subject at Mathematics for Program
Construction, and there is now a draft paper (pdf) available. The final
version will appear in Science of Computer Programming.
Ross Paterson maintains a web
page on arrows, including a nice proposal for adding syntactic
sugar to Haskell.
Sized Region Types
Lars Pareto and I have combined our earlier work on sized
types with Tofte and Talpin's region types. The
result is a type system for a small strict functional
language which can guarantee space bounds on the memory
needed to run the program -- even though the language has
both recursion and dynamic data structures. A paper
appeared at ICFP'99.
Here are some other papers:
Why Functional Programming
Matters, a tutorial paper on functional programming,
whose main thrust is that higher-order functions and lazy
evaluation can and should be used to make a substantial
contribution to modularity in functional programs. Dates
from 1984, but I suspect is probably still my most widely
read article! (bibtex).
A translation into Russian is now available!
Backwards Analysis of
Functional Programs, which suggests a framework for
analyses such as strictness analysis, escape analysis,
and sharing analysis, and a way of extending backwards
analysis to higher-order functions. This paper appeared
at the workshop on Partial Evaluation and Mixed
Computation in 1988. Warning: This is a scanned
version and it's BIG!
A Loop-detecting
Interpreter for Lazy, Higher-order Programs, a joint
paper with Alex Ferguson which appeared in the 1992
Glasgow Workshop on Functional Programming. The
interpreter described is based on Berry and Curien's
theory of sequential algorithms, and is able to detect a
surprising variety of loops. (bibtex).
Fast Abstract
Interpretation Using Sequential Algorithms, another
joint paper with Alex Ferguson which appeared in the
Workshop on Static Analysis, 1993. This paper uses
similar techniques to the previous one to find fixpoints
rapidly in the analysis of higher-order programs. (bibtex).
Projections
for strictness analysis, a joint paper with Phil
Wadler, which appeared in FPCA 1987. Describes a
method for backwards strictness analysis of first-order
programs with complex data structures, whose correctness
is argued by modelling contexts as projections. (bibtex).
Projections
for Polymorphic First-Order Strictness Analysis, a
joint paper with John Launchbury
which appeared in J. Mathematical Structures in Computer
Science in 1992. Applies categorical properties of
polymorphic functions to projection-based strictness
analysis, to show that analysing one instance yields
results that apply to all. (bibtex).
Avoiding
Unnecessary Updates, a joint paper with John Launchbury,
Andy Gill, Simon Marlow, Simon Peyton Jones, and Philip
Wadler, which appeared in the 1993 Glasgow Workshop on
Functional Programming. Describes a type-based analysis
to discover when the updates needed to implement
call-by-need are in fact unnecessary. (bibtex).
Reversing Abstract
Interpretations, a joint paper with John Launchbury
which appeared in ESOP in 1992. Shows how to `invert'
abstract functions using Galois connections, thus
reversing the direction of an analysis. We reverse Burn,
Hankin and Abramsky's strictness analysis and thereby
derive a more efficient (although less accurate)
backwards analysis from it. (bibtex).
The Design of a
Pretty-printing Library, a chapter for the Spring
School on Functional Programming. The library defines
five combinators for constructing documents with
alternative layouts, from which the `prettiest' is then
chosen. The combinators are specified formally and
several alternative implementations derived. The library
is distributed along with the Haskell B. compiler, and
the source is also available here.
(abstract, bibtex).
Haskell++:
An Object-Oriented Extension of Haskell, a joint
paper with Jan
Sparud which was presented at the Haskell Workshop in
1995. Haskell++ extends Haskell with `object classes' and
`object instances' which are analogous to the existing
classes and instances, but support inheritance. A simple preprocessor
translates into Haskell. Here is a ray-tracing
package in Haskell++, an undergraduate project. (bibtex).
Making
Choices Lazily, a joint paper with Andrew Moran
which appeared in FPCA
'95. It concerns the semantics of McCarthy's
bottom-avoiding choice in a language with call-by-need. (bibtex).
Proving the Correctness of
Reactive Systems Using Sized Types, a joint paper
with Lars
Pareto and Amr
Sabry, which appeared in POPL
'96. Sized types can express concepts such as 'lists
with at most 5 elements' and 'streams with at least 6
elements', and our type system can check properties such
as termination and liveness of programs in a simple lazy
functional language. (bibtex).
Restricted
Datatypes in Haskell, which appeared in the 1999
Haskell workshop. This paper proposes to improve
Haskell's support for data abstraction, by letting the
programmer declare that datatypes such as sets are well-formed
only under certain conditions on their element types.
These conditions then need not be repeated when the set
type is used, reducing the changes that must be made if
the set type is reimplemented with different
restrictions. The paper contains further applications and
shows how to implement Restricted Datatypes by a
translation into the Hugs extension of Haskell.
Binding-time Analysis for Polymorphic
Types (extended abstract), to appear in PSI 2001. This
joint paper with Rogardt Heldal extends
Dussart, Henglein and Mossin's work on polymorphic
binding-times to polymorphic types. Rogardt's thesis
contains much more detail.
Global
Variables in Haskell, which discusses how to implement updateable
global variables in Haskell. Management overview: use implicit
parameters. This is a draft; the final version will appear as a pearl in
JFP.
Here are the slides of a talk on the development of Erlang
that Joe Armstrong gave here recently. Much more than a
language description, it's full of thoughts on how to
introduce radically new technology in industry.
Here are some links to tutorial
papers on functional programming.