headers
Dino Distefano | 19 Dec 2009 19:17
Picon
Favicon

[TYPES/announce] Post-doc position (3 years) available at Queen Mary University of London

[ The Types Forum (announcements only), 
     http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

ONE POST DOCTORAL RESEARCH ASSISTANT
at Queen Mary university of London.

==================================================

Applications are invited for a full time Postdoctoral Research
Assistant within the Theory Group in the School of Electronic
Engineering and Compurter Science, to undertake research within
the context of an EPSRC funded project, "jStar: making Java
verification practical".

This project aims at theoretical and practical advances in Java
verification technology which will allow the extension of the
tool jStar to the stage where it can effectively reason about
programs with relatively complex correctness properties. In
particular, the project builds on our previous work on abstract
predicates families and automation of separation logic: see
http://www.cl.cam.ac.uk/~mjp41/jStar.

The project will be carried out in collaboration between the
Theory Group at Queen Mary University of
London (http://www.dcs.qmul.ac.uk/research/logic/) and the
Programming, Logic and Semantics Group at University of
Cambridge (http://www.cl.cam.ac.uk/research/pls/) in association
with Dr Matthew Parkinson.

The successful candidate would have a PhD in Computer Science,
(Continue reading)

Permalink | Reply | 0 comments |
headers
M.C.A. (Marco) Devillers | 25 Dec 2009 17:47
Picon

Operational Semantics Preserving Translations

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

I am looking for operational semantics preserving translations
regarding eager and lazily evaluated LC, where operational semantics
is purely defined on the side effects during the evaluation of a term.
I assume this shouldn't be too hard since one may assume these
functions exists since lambda evaluators can be written for each LC
with a certain operational semantics in each LC with a certain
semantics. At least, I hope I am correct in assuming so.

Assume a lambda calculus with side effects/impure function calls:

    M ::= c | v | \v . M | (M M) | call M*

Note that * is a sequence of terms. An example term: (\x. \y. call (+) x y) 2 3.

I define the operational semantics of a term as the series of calls
made to the system during the evaluation under a certain rewrite
strategy. Two terms evaluated under two rewrite strategies are
considered operationally equal if they made exactly the same calls in
exactly the same order.

What I am looking for are translation functions between lambda terms
of given form which map a lambda term given a certain rewrite strategy
to an operationally equivalent lambda term given another rewrite
strategy. I.e. say l makes a number of calls when lazily evaluated,
then I am looking for a translation function which gives a term l'
which, when evaluated eagerly, makes exactly the same calls in exactly
the same order. Of course, I am hoping for a linear translation.
(Continue reading)

Permalink | Reply | 0 comments |

Gmane