 Timestamp:
 Oct 25, 2012, 12:30:01 PM (9 years ago)
 Location:
 Papers
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

Papers/cppasm2012/cpp2012asm.tex
r2380 r2416 114 114 the rest of the assembler works in order to build globally correct solutions. 115 115 Proving their correctness is quite a complex task (see, for instance, 116 the compa ion paper~\cite{boender:correctness:2012}).116 the companion paper~\cite{boender:correctness:2012}). 117 117 Nevertheless, the correctness of the whole assembler only depends on the 118 118 correctness of the branch displacement algorithm. … … 365 365 The cost returned by the assembler for a pseudoinstruction is set to be the 366 366 cost 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 and367 as just shown, the costs of taking the true and false branches are different and 368 368 both need to be returned. 369 369 … … 396 396 \texttt{AJMP} if possible, or an \texttt{LJMP} otherwise, therefore always 397 397 picking the locally best solution. 398 In order to accom odate those optimal solutions that require local suboptimal399 choices, the policy may also return a boolean used to force398 In order to accommodate those optimal solutions that require local suboptimal 399 choices, the policy may also return a Boolean used to force 400 400 the translation of a \texttt{Jmp} into a \texttt{LJMP} even if 401 401 $\delta < 128$. An essentially identical mechanism exists for call … … 405 405 \texttt{a} by the policy and by the assembler must coincide. The latter is 406 406 the sum of the size of all the expansions of the pseudoinstructions that 407 prece edthe one at address \texttt{a}: the assembler just concatenates all407 precede the one at address \texttt{a}: the assembler just concatenates all 408 408 expansions sequentially. To grant this property, we impose a 409 409 correctness criterion over policies. A policy is correct when … … 445 445 Given a correct policy for the program to be assembled, the assembler never fails and returns some object code and a costing function. 446 446 Under the condition that the policy is `correct' for the program and the program is fully addressable by a 16bit word, the object code is also fully addressable by a 16bit word. 447 Moreover, the result of assembl ying 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)}.447 Moreover, 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)}. 448 448 449 449 Essentially the type above states that the \texttt{assembly} function correctly expands pseudoinstructions, and that the expanded instruction reside consecutively in memory. … … 680 680 Our source files are available at~\url{http://cerco.cs.unibo.it}. 681 681 We 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 focus sing on the main meat of the theorems.682 We 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. 683 683 We 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. 684 684 685 685 The complete development is spread across 29 files with around 20,000 lines of Matita source. 686 Rel avent files are: \texttt{AssemblyProof.ma}, \texttt{AssemblyProofSplit.ma} and \texttt{AssemblyProofSplitSplit.ma}, consisting of approximately 4500 lines of Matita source.686 Relevant files are: \texttt{AssemblyProof.ma}, \texttt{AssemblyProofSplit.ma} and \texttt{AssemblyProofSplitSplit.ma}, consisting of approximately 4500 lines of Matita source. 687 687 Numerous 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. 688 688 The low ratio between source lines and the number of lines of proof is unusual, but justified by the fact that the pseudoassembly and the assembly language share most constructs and large swathes of the semantics are shared. 
Papers/polymorphicvariants2012/polymorphicvariants.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 = {109139}, 7 volume = {39}, 8 issue = {2}, 9 year = {2007} 10 } 11 1 12 @inproceedings 2 13 { garrigue:code:2000, 
Papers/polymorphicvariants2012/polymorphicvariants.tex
r2414 r2416 94 94 \begin{minipage}[b]{0.45\linewidth} 95 95 \begin{lstlisting} 96 96 97 \end{lstlisting} 97 98 \end{minipage} … … 123 124 \subsection{Matita} 124 125 \label{subsect.matita} 126 127 Matita~\cite{asperti:user:2007} is a dependentlytyped proof assistant developed in Bologna, implementing the Calculus of (Co)inductive Constructions, a type theory similar to that of Coq. 128 Throughout this paper, all running examples are provided in Matita's proof script vernacular. 129 This vernacular, similar to the syntax of OCaml or Coq, should be mostly straightforward. 130 131 One possible source of confusion is our use of $?$ and $\ldots$, which correspond to a term, or terms, to be inferred automatically by unification, respectively. 132 Any terms that cannot be inferred by unification from the surrounding context are left for the user to provide as proof obligations. 133 134 Matita 125 135 126 136 \subsection{Subtyping as instantiation vs subtyping as safe static cast}
Note: See TracChangeset
for help on using the changeset viewer.