| #
d765a64b |
|
16-May-2016 |
Thomas Sewell <Thomas.Sewell@nicta.com.au> |
SELFOUR-444: Haskell implementation, begin refine.
First attempt at a haskell implementation of preemptible retyping
and the refinement proof to abstract.
|
| #
fad2c6aa |
|
11-Jan-2016 |
Daniel Matichuk <daniel.matichuk@nicta.com.au> |
paramatrised abstract and haskell specs over L4V_ARCH
Haskell translator was modified to support multiple translations
of the haskell, with different build parameters.
|
| #
7e40646c |
|
01-Dec-2015 |
Thomas Sewell <Thomas.Sewell@nicta.com.au> |
Proof up to Fastpath_C.
The very last twist of this: the proof that resolveAddressBits can
be seen as functional needs to change, a lot, because it's now
sensitive to gsCNodes. Still working on that.
|
| #
12fa8686 |
|
16-May-2015 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
fewer warnings
|
| #
2a03e81d |
|
14-Jul-2014 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
Import release snapshot.
|