Changeset 1435 for Deliverables


Ignore:
Timestamp:
Oct 21, 2011, 5:24:08 PM (8 years ago)
Author:
sacerdot
Message:

More on dependent types. One citation is missing.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.2-4.3/reports/D4-2.tex

    r1434 r1435  
    330330\label{subsect.use.of.dependent.types}
    331331
    332 We see two potential ways in which a compiler can fail to compile a program:
     332We see several potential ways in which a compiler can fail to compile a program:
    333333\begin{enumerate}
    334334\item
    335335The program is malformed, and there is no hope of making sense of the program.
    336336\item
    337 The compiler is buggy, or an invariant in the compiler is invalidated, for example, if the program is too large to fit into the processor's code memory.
     337The compiler is buggy, or an invariant in the compiler is invalidated.
     338\item Some non complete heuristics in the compiler fails.
     339\item The compiled code exhausts some bounded resource, tipically the
     340processor's code memory.
    338341\end{enumerate}
     342Standard compilers can fail for all the above reasons. Certified compilers
     343are only required to rule out the second class of failures, but they can
     344still fail for all other reasons. In particular, a compiler that systematically
     345refuses to compile any well formed program is a sound compiler. On the contrary,
     346we would like our certified compiler to fail only in the fourth case. We
     347plan to achieve this aim using the following strategy. First of all,
     348the compiler is abstracted over all non complete heuristics, seen as total
     349functions. To obtain an executable code, the compiler is eventually composed
     350with implementations of the strategies, and the composition takes care of the
     351possibility that the heuristics can fail to find a solution. Secondly,
     352we will reject all malformed programs using dependent types:
     353only well-formed programs should typecheck and the compiler can be applied only
     354to well-typed programs. Finally, exhaustion of bounded resources can be checked
     355only at the very end of the compilation. Therefore, all intermediate compilation
     356steps are now total functions that cannot diverge, nor fail: these properties
     357are directly guaranteed by the type system of Matita.
     358
     359At the moment, the plan has not been fulfilled, and we are improving the code
     360according to the plan by progressively strenghthening the code by means of
     361dependent types. We now detail the different ways in which dependent types
     362have been exploited so far.
     363
    339364First, we encode informal invariants, or uses of \texttt{assert false} in the O'Caml code, with dependent types, converting partial functions into total functions.
    340365There are numerous examples of this throughout the backend.
     
    370395\end{lstlisting}
    371396Here, \texttt{codeT} is a parameterised type representing the `structure' of the function's body (a graph in graph based languages, and a list in the linearised LIN language).
    372 Specifically, the \texttt{joint\_if\_entry} is a dependent pair consisting of a label and a proof that the label in question is a vertex in the function's graph.
    373 A similar device exists for the exit label.
    374 
    375 Finally, we make use of dependent types for another reason: experimentation.
     397Specifically, the \texttt{joint\_if\_entry} is a dependent pair consisting of a label and a proof that the label in question is a vertex in the function's graph. A similar device exists for the exit label.
     398
     399We make use of dependent types also for another reason: experimentation.
    376400Namely, CompCert makes little use of dependent types to encode invariants.
    377401In contrast, we wish to make as much use of dependent types as possible, both to experiment with different ways of encoding compilers in a proof assistant, but also as a way of `stress testing' Matita's support for dependent types.
    378 In particular, we would like to make use of Matita's support for `Russell'-style reasoning.
     402
     403Moreover, at the moment we make practically no use of inductive predicates
     404to specify compiler invariants and to describe the semantics of intermediate
     405languages. On the contrary, all predicates are computable functions. Therefore,
     406the proof style that we will adopt will be necessarily significantly different
     407from, say, CompCert's one. At the moment, in Matita ``Russell-''-style reasoning
     408(in the sense of~\cite{sozeauXXX}) seems to be the best solution to work on
     409computable functions. This style is heavily based on the idea that all
     410computable functions should be specified using dependent types to describe
     411their pre and post-conditions. As a consequence, it is natural to add
     412dependent types almost everywhere in the code.
    379413
    380414%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
Note: See TracChangeset for help on using the changeset viewer.