Changeset 2416 for Papers


Ignore:
Timestamp:
Oct 25, 2012, 12:30:01 PM (7 years ago)
Author:
mulligan
Message:

Some more minor changes

Location:
Papers
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • Papers/cpp-asm-2012/cpp-2012-asm.tex

    r2380 r2416  
    114114the rest of the assembler works in order to build globally correct solutions.
    115115Proving their correctness is quite a complex task (see, for instance,
    116 the compaion paper~\cite{boender:correctness:2012}).
     116the companion paper~\cite{boender:correctness:2012}).
    117117Nevertheless, the correctness of the whole assembler only depends on the
    118118correctness of the branch displacement algorithm.
     
    365365The cost returned by the assembler for a pseudoinstruction is set to be the
    366366cost of its expansion in clock cycles. For conditional jumps that are expanded
    367 as just shown, the costs of takin the true and false branches are different and
     367as just shown, the costs of taking the true and false branches are different and
    368368both need to be returned.
    369369
     
    396396\texttt{AJMP} if possible, or an \texttt{LJMP} otherwise, therefore always
    397397picking the locally best solution.
    398 In order to accomodate those optimal solutions that require local sub-optimal
    399 choices, the policy may also return a boolean used to force
     398In order to accommodate those optimal solutions that require local sub-optimal
     399choices, the policy may also return a Boolean used to force
    400400the translation of a \texttt{Jmp} into a \texttt{LJMP} even if
    401401$\delta < 128$. An essentially identical mechanism exists for call
     
    405405\texttt{a} by the policy and by the assembler must coincide. The latter is
    406406the sum of the size of all the expansions of the pseudo-instructions that
    407 preceed the one at address \texttt{a}: the assembler just concatenates all
     407precede the one at address \texttt{a}: the assembler just concatenates all
    408408expansions sequentially. To grant this property, we impose a
    409409correctness criterion over policies. A policy is correct when
     
    445445Given a correct policy for the program to be assembled, the assembler never fails and returns some object code and a costing function.
    446446Under the condition that the policy is `correct' for the program and the program is fully addressable by a 16-bit word, the object code is also fully addressable by a 16-bit word.
    447 Moreover, the result of assemblying the pseudoinstruction obtained fetching from the assembly address \texttt{ppc} is a list of bytes found in the generated object code starting from the object code address \texttt{policy(ppc)}.
     447Moreover, the result of assembling the pseudoinstruction obtained fetching from the assembly address \texttt{ppc} is a list of bytes found in the generated object code starting from the object code address \texttt{policy(ppc)}.
    448448
    449449Essentially the type above states that the \texttt{assembly} function correctly expands pseudoinstructions, and that the expanded instruction reside consecutively in memory.
     
    680680Our source files are available at~\url{http://cerco.cs.unibo.it}.
    681681We assumed several properties of `library functions', e.g. modular arithmetic and datastructure manipulation.
    682 We axiomatised various small functions needed to complete the main theorems, as well as some `routine' proof obligations of the theorems themselves, in focussing on the main meat of the theorems.
     682We axiomatised various small functions needed to complete the main theorems, as well as some `routine' proof obligations of the theorems themselves, in focusing on the main meat of the theorems.
    683683We believe that the proof strategy is sound and that all axioms can be closed, up to minor bugs that should have local fixes that do not affect the global proof strategy.
    684684
    685685The complete development is spread across 29 files with around 20,000 lines of Matita source.
    686 Relavent files are: \texttt{AssemblyProof.ma}, \texttt{AssemblyProofSplit.ma} and \texttt{AssemblyProofSplitSplit.ma}, consisting of approximately 4500 lines of Matita source.
     686Relevant files are: \texttt{AssemblyProof.ma}, \texttt{AssemblyProofSplit.ma} and \texttt{AssemblyProofSplitSplit.ma}, consisting of approximately 4500 lines of Matita source.
    687687Numerous other lines of proofs are spread all over the development because of dependent types and the Russell proof style, which does not allow one to separate the code from the proofs.
    688688The low ratio between source lines and the number of lines of proof is unusual, but justified by the fact that the pseudo-assembly and the assembly language share most constructs and large swathes of the semantics are shared.
  • Papers/polymorphic-variants-2012/polymorphic-variants.bib

    r2414 r2416  
     1@article
     2{ asperti:user:2007,
     3  author = {Andrea Asperti and Claudio {Sacerdoti Coen} and Enrico Tassi and Stefano Zacchiroli},
     4  title = {User interaction with the {Matita} proof assistant},
     5  journal = {Automated Reasoning},
     6  pages = {109--139},
     7  volume = {39},
     8  issue = {2},
     9  year = {2007}
     10}
     11
    112@inproceedings
    213{ garrigue:code:2000,
  • Papers/polymorphic-variants-2012/polymorphic-variants.tex

    r2414 r2416  
    9494\begin{minipage}[b]{0.45\linewidth}
    9595\begin{lstlisting}
     96
    9697\end{lstlisting}
    9798\end{minipage}
     
    123124\subsection{Matita}
    124125\label{subsect.matita}
     126
     127Matita~\cite{asperti:user:2007} is a dependently-typed proof assistant developed in Bologna, implementing the Calculus of (Co)inductive Constructions, a type theory similar to that of Coq.
     128Throughout this paper, all running examples are provided in Matita's proof script vernacular.
     129This vernacular, similar to the syntax of OCaml or Coq, should be mostly straightforward.
     130
     131One possible source of confusion is our use of $?$ and $\ldots$, which correspond to a term, or terms, to be inferred automatically by unification, respectively.
     132Any terms that cannot be inferred by unification from the surrounding context are left for the user to provide as proof obligations.
     133
     134Matita
    125135
    126136\subsection{Subtyping as instantiation vs subtyping as safe static cast}
Note: See TracChangeset for help on using the changeset viewer.