Sun Mar 7 22:56:47 CET 2010
The basic idea is that a compiler is a function, i.e. implemented by a
collection of rewrite rules, that relates one syntactic domain to
In order to verify correctness of this ``arrow'' the language needs a
formal model - another arrow - to compare it with.
language -----> machine code
| definitional | machine code
| interpreter | interpreter
abstract domain (i.e. Haskell functions)
That's my idea. How does  do it? In each pass (14 passes and 8
intermediate languages) the semantics of the language is defined, and
the transformation is proven to preserve the semantics.
I am only interested in one pass: the reductions used in the PIC18
instruction selection. It looks like I need a Hoare logic for the
machine opcodes, i.e. some kind of typing rules for the state
transitions, and how they can be composed.
So, my question is: in the spirit of tagless interpreters, is it
possible to write down the Staapl PIC18 reduction rules such that:
* PIC18 Instruction semantics can be encoded in the type as much as
possible. I.e. data dependencies.
* Remaining semantics (i.e. add or sub) is encoded in behaviour, and
can be verified by quickcheck.
Doing this in Scheme as an alternative to encoding it in Haskell/OCaml
type system is probably also possible, but I would need to make a