Ewen Denney
I have worked in IRISA (Rennes), Hong Kong Baptist University, and the University of Edinburgh.
I am interested in mathematical foundations and tool support for
formal
program development. Specific interests include program synthesis, Java
Card, numerical algorithms, and the Palm OS.
My previous page in the
Lande group at Irisa, in Rennes.
Research
Program Synthesis
- The Synthesis of a Java Card Tokenisation Algorithm : ps
- Logic-based Program Synthesis via Program Extraction : pdf
Proof Assistants
A first stab at an automatic translator from HOL to Coq.
- A Prototype Proof Translator from HOL to Coq : ps
Current Interests
- A framework for tactic languages
- Abstraction in constructive logic
- Proof mining
Java Card
The Java Card language is a dialect of Java, designed for programming
smart
cards. The core language is a subset of Java. This has been extended
with
various libraries (APIs in Java terminology) with specific
functionality
for smart cards. Smart cards are an important challenge for formal
methods
for two reasons. Firstly, since code is installed on the cards
themselves,
the cost of correcting errors could be enormous. Secondly, due to the
memory
and processing constraints, programs are actually quite small and so
amenable
to formal reasoning.
We are studying formal
aspects of Java Card. We have given a bytecode semantics and used
this
to prove the correctness
of a particular optimisation of the virtual machine. We are
concentrating
now on the formal development of an optimiser. Future work will include
extending our formalisation to the runtime environment.
A talk
(in French) giving an overview of Java Card.
- The Synthesis of a Java Card Tokenisation Algorithm : ps,
bib
- An Operational Semantics of the Java Card Firewall : ps,
pdf
- Correctness of Java Card Method Lookup via Logical Relations
(journal version)
: ps
- Correctness of Java Card Method Lookup via Logical Relations
(conference)
: ps,
bib
- Correctness of Java Card Tokenisation (longer tech report) :
ps,
pdf
Refinement
More about my research
on refinement.
- A Theory of Program Refinement : ps,
pdf,
abstract,
bib
My thesis was on the theory of refinement calculi, with an eye
on how choices made in the formalism have a bearing on practical
issues.
Program refinement is a formal method in which a program is
gradually
derived from a specification, using rules of a calculus in which the
intermediate
stages of development are recorded. Refinement is not a program
development
methodology, as such, but rather a framework for recording and reusing
developments, and so should be seen as part of a larger framework for
programming
as a whole. In my thesis, I studied the theoretical issues which arise
in its formalisation, by working with a simple idealised language and
program
logic, and formalising the refinement theory this induces together with
its semantics. The refinement calculus is a lambda-calculus extended
with
existential variables and first-order logic. We prove that this is
conservative
over the underlying logic.
- Simply-typed Underdeterminism :
ps,
bib
An extension of the simply-typed lambda calculus for formalising the
concept of underdeterminism. This allows us to express stubs
and
skeletons which give rise to the notion of partiality in top-down
program
and proof development. We axiomatise a simple notion of program
refinement
and give a semantics, for which the calculus is proven sound and
complete.
- Refinement Types for Specification : ps,
bib
A theory of program specification based on the notion of refinement
type. This provides a notion of structured specification. We
axiomatise
the satisfaction of specifications by programs as a generalised typing
relation and give rules for refining specifications. A per semantics
based
on Henkin models is given, and the calculus proven sound and complete.
- Refining Refinement Types :
ps,
abstract,
bib,
More details and a slightly different semantics.
Last
modified: Tue Nov 20 18:25:14 GMT 2001