Changeset 1202


Ignore:
Timestamp:
Sep 9, 2011, 11:48:34 AM (8 years ago)
Author:
mulligan
Message:

more changes, changed mention of atkey's jvm

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/ITP-Paper/itp-2011.tex

    r1201 r1202  
    781781Even from a technical level the two formalisations differ: we use dependent types whilst CompCert largely sticks to non-dependent types.
    782782
    783 In~\cite{atkey:coqjvm:2007} an executable specification of the Java Virtual Machine, using dependent types, is presented.
    784 As we do, dependent types there are used to remove spurious partiality from the model.
    785 They also lower the need for over-specifying the behaviour of the processor in impossible cases.
    786 Our use of dependent types will also help to maintain invariants when we prove the correctness of the CerCo prototype C compiler.
     783Atkey~\cite{atkey:coqjvm:2007} provides an executable specification of the JVM.
     784Dependent types are used to remove spurious partiality from the model, and lower the need for over-specifying the behaviour of the processor in impossible cases.
     785However, dependent types in the two formalisations are used differently.
     786Further, our use of dependent types will also serve to enforce invariants in the CerCo compiler.
    787787
    788788Finally~\cite{sarkar:semantics:2009} provides an executable semantics for x86-CC multiprocessor machine code.
Note: See TracChangeset for help on using the changeset viewer.