Changeset 1199
 Timestamp:
 Sep 9, 2011, 9:49:44 AM (8 years ago)
 Location:
 Deliverables/D4.1/ITPPaper
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/ITPPaper/itp2011.bib
r819 r1199 1 1 @article 2 2 { asperti:user:2007, 3 author = {A ndrea Asperti and Claudio Sacerdoti Coen and Enrico Tassi and StefanoZacchiroli},3 author = {A. Asperti and C. Sacerdoti Coen and E. Tassi and S. Zacchiroli}, 4 4 title = {User interaction with the {Matita} proof assistant}, 5 journal = { Journal ofAutomated Reasoning},5 journal = {Automated Reasoning}, 6 6 pages = {109139}, 7 7 volume = {39}, … … 12 12 @article 13 13 { bate:wcet:2011, 14 author = {I ain Bate and UsmanKhan},14 author = {I. Bate and U. Khan}, 15 15 title = {{WCET} analysis of modern processors using multicriteria optimisation}, 16 16 journal = {Empirical Software Engineering}, … … 23 23 @article 24 24 { leroy:formal:2009, 25 author = {X avierLeroy},25 author = {X. Leroy}, 26 26 title = {Formal verification of a realistic compiler}, 27 journal = {C ommunications of the {Association of Computing Machinery}},27 journal = {CACM}, 28 28 volume = {52}, 29 29 number = {7}, … … 34 34 @article 35 35 { leroy:formally:2009, 36 author = {X avierLeroy},36 author = {X. Leroy}, 37 37 title = {A formally verified compiler backend}, 38 journal = { Journal ofAutomated Reasoning},38 journal = {Automated Reasoning}, 39 39 volume = {43}, 40 40 number = {4}, … … 45 45 @article 46 46 { luo:coercive:1999, 47 author = {Z haohuiLuo},47 author = {Z. Luo}, 48 48 title = {Coercive subtyping}, 49 journal = { Journal ofLogic and Computation},49 journal = {Logic and Computation}, 50 50 volume = {9}, 51 51 number = {1}, … … 56 56 @inproceedings 57 57 { yan:wcet:2008, 58 author = {J un Yan and WeiZhang},58 author = {J. Yan and W. Zhang}, 59 59 title = {{WCET} Analysis for MultiCore Processors with Shared {L2} Instruction Caches}, 60 booktitle = { $\mathrm{14^{th}}$ {IEEE} Symposium on Realtime and Embedded Technology and Applications},60 booktitle = {{RTAS}}, 61 61 pages = {8089}, 62 62 year = {2008} … … 65 65 @inproceedings 66 66 { atkey:coqjvm:2007, 67 author = {R obertAtkey},67 author = {R. Atkey}, 68 68 title = {{CoqJVM}: An executable specification of the {Java Virtual Machine} using dependent types}, 69 booktitle = { Conference of the {TYPES} Project},69 booktitle = {{TYPES}}, 70 70 pages = {1832}, 71 71 year = {2007} … … 75 75 { blanqui:designing:2010, 76 76 title = {Designing a {CPU} model: from a pseudoformal document to fast code}, 77 author = {F r\'ed\'eric Blanqui and Claude Helmstetter and Vania Joloboff and JeanFran\c{c}ois Monin and XiaomuShi},78 booktitle = { $\mathrm{3^{rd}}$ Workshop on Rapid Simulation and Performance Evaluation: Methods and Tools},77 author = {F. Blanqui and C. Helmstetter and V. Joloboff and J. Monin and X. Shi}, 78 booktitle = {{RAPIDO}}, 79 79 year = {2010} 80 80 } … … 82 82 @inproceedings 83 83 { blazy:formal:2006, 84 author = {S andrine Blazy and Zaynah Dargaye and XavierLeroy},84 author = {S. Blazy and Z. Dargaye and X. Leroy}, 85 85 title = {Formal Verification of a {C} Compiler FrontEnd}, 86 booktitle = { International Symposium on Formal Methods},86 booktitle = {FM}, 87 87 pages = {460475}, 88 88 year = {2006} … … 91 91 @inproceedings 92 92 { chlipala:verified:2010, 93 author = {A damChlipala},93 author = {A. Chlipala}, 94 94 title = {A verified compiler for an impure functional language}, 95 booktitle = { $\mathrm{37^{th}}$ Annual Symposium on Principles of Programming Languages},95 booktitle = {POPL}, 96 96 pages = {93106}, 97 97 year = {2010} … … 100 100 @inproceedings 101 101 { fox:trustworthy:2010, 102 author = {A nthony Fox and MagnusO. Myreen},102 author = {A. Fox and M. O. Myreen}, 103 103 title = {A Trustworthy Monadic Formalization of the {ARMv7} Instruction Set Architecture}, 104 booktitle = { $\mathrm{1^{st}}$ International Conference on Interactive Theorem Proving},104 booktitle = {ITP}, 105 105 pages = {243258}, 106 106 year = {2010} … … 109 109 @inproceedings 110 110 { garrigue:programming:1998, 111 author = {J acquesGarrigue},111 author = {J. Garrigue}, 112 112 title = {Programming with polymorphic variants}, 113 113 booktitle = {{ML} Workshop}, … … 117 117 @inproceedings 118 118 { leijen:domain:1999, 119 author = {D aan Leijen and ErikMeijer},119 author = {D. Leijen and E. Meijer}, 120 120 title = {Domain specific embedded compilers}, 121 booktitle = { $\mathrm{2^{nd}}$ Conference on Domain Specific Languages},121 booktitle = {DSL}, 122 122 pages = {109122}, 123 123 year = {1999} … … 126 126 @inproceedings 127 127 { sarkar:semantics:2009, 128 author = {S usmit Sarkar and Peter Sewell and Francesco Zappa Nardelli and Scott Owens and Tom Ridge and Thomas Braibant and Magnus O. Myreen and JadeAlglave},128 author = {S. Sarkar and P. Sewell and F. Zappa Nardelli and S. Owens and T. Ridge and T. Braibant and M. O. Myreen and J. Alglave}, 129 129 title = {The semantics of {x86CC} multiprocessor machine code}, 130 booktitle = { $\mathrm{36^{th}}$ Annual Symposium on Principles of Programming Languages},130 booktitle = {POPL}, 131 131 pages = {379391}, 132 132 year = {2009} … … 135 135 @inproceedings 136 136 { shankar:principles:1999, 137 author = {N atarajan Shankar and SamOwre},137 author = {N. Shankar and S. Owre}, 138 138 title = {Principles and Pragmatics of Subtyping in {PVS}}, 139 139 booktitle = {Recent Trends in Algebraic Development Techniques}, … … 144 144 @inproceedings 145 145 { sozeau:subset:2006, 146 author = {M atthieuSozeau},146 author = {M. Sozeau}, 147 147 title = {Subset coercions in {Coq}}, 148 booktitle = { Conference of the {TYPES} Project},148 booktitle = {{TYPES}}, 149 149 pages = {237252}, 150 150 year = {2006} … … 153 153 @inproceedings 154 154 { xi:guarded:2003, 155 author = {H ongwei Xi and Chiyan Chen and GangChen},155 author = {H. Xi and C. Chen and G. Chen}, 156 156 title = {Guarded recursive datatype constructors}, 157 booktitle = { $\mathrm{30^{th}}$ Annual Symposium on Principles of Programming Languages},157 booktitle = {POPL}, 158 158 pages = {224235}, 159 159 year = {2003} … … 162 162 @misc 163 163 { cerco:2011, 164 title = {The {CerCo} {FETOpen}Project},164 title = {The {CerCo} Project}, 165 165 howpublished = {\url{http://cerco.cs.unibo.it}}, 166 166 year = {2011}, … … 186 186 @misc 187 187 { moore:grand:2005, 188 author = {J S trotherMoore},188 author = {J S. Moore}, 189 189 title = {A Grand Challenge Proposal for Formal Methods}, 190 190 year = {2005} … … 193 193 @misc 194 194 { oliboni:matita:2008, 195 author = {C osimoA. Oliboni},195 author = {C. A. Oliboni}, 196 196 title = {{Matita} come Supporto per Specifiche Eseguibili: Formalizzazione Interattiva dei Microcontroller a 8 bit {Freescale}}, 197 institution = { Dipartimento di Scienze dell'Informazione,Universit\`a di Bologna},197 institution = {Universit\`a di Bologna}, 198 198 howpublished = {\url{http://matita.cs.unibo.it/library.shtml}}, 199 199 year = {2008} … … 218 218 @techreport 219 219 { amadio:certifying:2010, 220 author = {R oberto M. Amadio and Nicolas Ayache and Yann R\'{e}gisGianas and RonanSaillard},220 author = {R. M. Amadio and N. Ayache and Y. R\'{e}gisGianas and R. Saillard}, 221 221 title = {Cerifying cost annotations in compilers}, 222 institution = {Universit\'{e} Paris Diderot {(Paris 7)}, Laboratoire {PPS}},223 year = {2010} 224 } 222 institution = {Universit\'{e} Paris Diderot}, 223 year = {2010} 224 } 
Deliverables/D4.1/ITPPaper/itp2011.tex
r1190 r1199 36 36 mathescape=true, 37 37 } 38 \lstset{language=matitaocaml,basicstyle=\ tt,columns=flexible,breaklines=false,38 \lstset{language=matitaocaml,basicstyle=\scriptsize\tt,columns=flexible,breaklines=false, 39 39 keywordstyle=\bfseries, %\color{red}\bfseries, 40 40 keywordstyle=[2]\bfseries, %\color{blue}, … … 54 54 } 55 55 56 \setlength{\belowcaptionskip}{0pt} 57 \setlength{\textfloatsep}{1em} 58 56 59 \begin{document} 57 60 58 61 \author{Dominic P. Mulligan \and Claudio Sacerdoti Coen} 59 62 \authorrunning{D. P. Mulligan \and C. Sacerdoti Coen} 60 \institute{Dipartimento di Scienze dell'Informazione,\\ Universit\`a di Bologna} 61 %\and 62 % \IEEEauthorblockN{Claudio Sacerdoti Coen} 63 % \IEEEauthorblockA{Dipartimento di Scienze dell'Informazione,\\ Universit\`a di Bologna} 64 %} 63 \institute{\vspace{2em}} 64 % \institute{Dipartimento di Scienze dell'Informazione,\\ Universit\`a di Bologna} 65 65 66 66 \bibliographystyle{plain} … … 82 82 \end{abstract} 83 83 84 \begin{keywords}85 Hardware formalisation, Matita, dependent types, CerCo86 \end{keywords}84 %\begin{keywords} 85 %Hardware formalisation, Matita, dependent types, CerCo 86 %\end{keywords} 87 87 88 88 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% … … 395 395 inductive BitVectorTrie(A: Type[0]):nat $\rightarrow$ Type[0] := 396 396 Leaf: A $\rightarrow$ BitVectorTrie A 0 397  Node: ∀n. BitVectorTrie A n $\rightarrow$ BitVectorTrie A n $\rightarrow$ 398 BitVectorTrie A (S n) 397  Node: ∀n. BitVectorTrie A n $\rightarrow$ BitVectorTrie A n $\rightarrow$ BitVectorTrie A (S n) 399 398  Stub: ∀n. BitVectorTrie A n. 400 399 \end{lstlisting} … … 473 472 These costs are taken from a Siemens Semiconductor Group data sheet for the MCS51~\cite{siemens:2011}, and will likely vary between particular implementations. 474 473 \begin{lstlisting}[frame=single] 475 definition fetch: BitVectorTrie Byte 16 $\rightarrow$ Word $\rightarrow$ 476 instruction $\times$ Word $\times$ nat 474 definition fetch: BitVectorTrie Byte 16 $\rightarrow$ Word $\rightarrow$ instruction $\times$ Word $\times$ nat 477 475 \end{lstlisting} 478 476 Instruction are assembled to bit encodings by \texttt{assembly1}: … … 484 482 A map associating memory locations and cost labels (see Subsection~\ref{subsect.computation.cost.traces}) is produced. 485 483 \begin{lstlisting}[frame=single] 486 definition assembly: assembly_program $\rightarrow$ 487 option (list Byte $\times$ (BitVectorTrie String 16)) 484 definition assembly: assembly_program $\rightarrow$ option (list Byte $\times$ (BitVectorTrie String 16)) 488 485 \end{lstlisting} 489 486 A single fetchdecodeexecute cycle is performed by \texttt{execute\_1}: … … 523 520 [ `ADD of acc * [ reg  direct  indirect  data ] 524 521 ... 525  `MOV of 526 (acc * [ reg direct  indirect  data ], 522  `MOV of (acc * [ reg direct  indirect  data ], 527 523 [ reg  indirect ] * [ acc  direct  data ], 528 524 direct * [ acc  reg  direct  indirect  data ], … … 535 531 Here, \texttt{union6} is a disjoint union type, defined as follows: 536 532 \begin{lstlisting} 537 type ('a,'b,'c,'d,'e,'f) union6 = 538 [ `U1 of 'a  ...  `U6 of 'f ] 533 type ('a,'b,'c,'d,'e,'f) union6 = [ `U1 of 'a  ...  `U6 of 'f ] 539 534 \end{lstlisting} 540 535 The types \texttt{union2}, \texttt{union3} and \texttt{union6} sufficed. … … 566 561 $\lambda$d: addressing_mode_tag. $\lambda$A: addressing_mode. 567 562 match d with 568 [ direct $\Rightarrow$ 569 match A with [ DIRECT _ $\Rightarrow$ true  _ $\Rightarrow$ false ] 570  indirect $\Rightarrow$ 571 match A with [ INDIRECT _ $\Rightarrow$ true  _ $\Rightarrow$ false ] 563 [ direct $\Rightarrow$ match A with [ DIRECT _ $\Rightarrow$ true  _ $\Rightarrow$ false ] 564  indirect $\Rightarrow$ match A with [ INDIRECT _ $\Rightarrow$ true  _ $\Rightarrow$ false ] 572 565 ... 573 566 \end{lstlisting} … … 577 570 A \texttt{subaddressing\_mode} is an \emph{ad hoc} nonempty $\Sigma$type of \texttt{addressing\_mode}s in a set of tags: 578 571 \begin{lstlisting}[frame=single] 579 record subaddressing_mode 580 (n: nat) 581 (l: Vector addressing_mode_tag (S n)): Type[0] := 582 { 572 record subaddressing_mode (n: nat) (l: Vector addressing_mode_tag (S n)): Type[0] := { 583 573 subaddressing_modeel :> addressing_mode; 584 subaddressing_modein: 585 bool_to_Prop (is_in $\ldots$ l subaddressing_modeel) 574 subaddressing_modein: bool_to_Prop (is_in $\ldots$ l subaddressing_modeel) 586 575 }. 587 576 \end{lstlisting} … … 589 578 \begin{lstlisting}[frame=single] 590 579 inductive preinstruction (A: Type[0]): Type[0] ≝ 591 ADD: $\llbracket$acc_a$\rrbracket$ $\rightarrow$ $\llbracket$register;direct;indirect;data$\rrbracket$ $\rightarrow$ 592 preinstruction A 593  ADDC: $\llbracket$acc_a$\rrbracket$ $\rightarrow$ $\llbracket$register;direct;indirect;data$\rrbracket$ $\rightarrow$ 594 preinstruction A 580 ADD: $\llbracket$acc_a$\rrbracket$ $\rightarrow$ $\llbracket$register;direct;indirect;data$\rrbracket$ $\rightarrow$ preinstruction A 581  ADDC: $\llbracket$acc_a$\rrbracket$ $\rightarrow$ $\llbracket$register;direct;indirect;data$\rrbracket$ $\rightarrow$ preinstruction A 595 582 ... 596 583 \end{lstlisting} … … 656 643 type line = 657 644 [ `P1 of byte  `P3 of byte 658  `SerialBuff of 659 [ `Eight of byte 660  `Nine of BitVectors.bit * byte ] ] 645  `SerialBuff of [ `Eight of byte  `Nine of BitVectors.bit * byte ] ] 646 661 647 type continuation = 662 [`In of time * line * 663 epsilon * continuation] option * 648 [`In of time * line * epsilon * continuation] option * 664 649 [`Out of (time > line > time * continuation)] 665 650 \end{lstlisting}
Note: See TracChangeset
for help on using the changeset viewer.