<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
@inproceedings{alglave+:powerarm09,
  author =       {Jade Alglave and 
                  Anthony Fox and 
                  Samin Ishtiaq and 
                  Magnus O. Myreen and 
                  Susmit Sarkar and 
                  Peter Sewell and 
                  Zappa Nardelli, Francesco},
  title =        {The Semantics of {Power} and {ARM} Multiprocessor Machine Code},
  year =         {2009},
  booktitle =    {{DAMP} 2009: Workshop on Declarative Aspects of Multicore Programming},
  month =        jan,
  note = {(12 page extended abstract)},
}

@inproceedings{crary+:mafcc-cade,
  author    = {Karl Crary and
               Susmit Sarkar},
  title     = {Foundational Certified Code in a Metalogical Framework},
  booktitle = {International Conference on Automated Deduction},
  year      = {2003},
  pages     = {106-120},
  series    = {Lecture Notes in Computer Science},
  volume    = {2741},
  isbn      = {3-540-40559-3},
}

@article{crary+:mafcc,
  author    = {Karl Crary and Susmit Sarkar},
  title     = {Foundational certified code in the {Twelf} metalogical framework},
  journal   = {{ACM} Transactions on Computatational Logic ({TOCL})},
  volume    = {9},
  number    = {3},
  year      = {2008},
  ee        = {http://doi.acm.org/10.1145/1352582.1352584},
}

@techreport{crary+:mafcc-tr,
  author = {Karl Crary and Susmit Sarkar},
  title = {Foundational certified code in a metalogical framework},
  institution = cmu-cs,
  year = 2003,
  number = {CMU-CS-03-108},
}

@inproceedings{owens+:x86tso,
  author    = {Scott Owens and Susmit Sarkar and Peter Sewell},
  title     = {A better x86 memory model: {x86-TSO}},
  booktitle = {Proceedings of Theorem Proving in Higher Order Logics (TPHOLs)},
  year      = {2009},
  pages     = {391--407},
  series    = {Lecture Notes in Computer Science},
  volume    = {5674},
  ee        = {http://dx.doi.org/10.1007/978-3-642-03359-9_27},
}

@techreport{owens+:x86tso-tr745,
  author =       {Scott Owens and Susmit Sarkar and Peter Sewell},
  title =        {A better x86 memory model: {x86-TSO} (extended version)},
  institution =  {Univ.\ of Cambridge},
  year =         {2009},
  number =       {UCAM-CL-TR-745},
  note =         {Supporting material at~\url{www.cl.cam.ac.uk/users/pes20/weakmemory/}},
}

@inproceedings{sarkar+:oracle,
  author    = {Susmit Sarkar and
               Brigitte Pientka and
               Karl Crary},
  title     = {Small Proof Witnesses for {LF}},
  booktitle = {International Conference on Logic Programming},
  title     = {Small Proof Witnesses for {LF}},
  booktitle = {Proceedings of the International Conference on Logic
                  Programming (ICLP)},
  year      = {2005},
  pages     = {387--401},
  series    = {Lecture Notes in Computer Science},
  volume    = {3668},
  isbn      = {3-540-29208-X},
  ee        = {http://dx.doi.org/10.1007/11562931_29},
}

@inproceedings{sarkar+:ottbinding,
  author =       {Susmit Sarkar and 
                  Peter Sewell and 
                  Zappa Nardelli, Francesco},
  title =        {Specifying real-world binding structures},
  booktitle =    {2nd Informal {ACM} {SIGPLAN} Workshop on Mechanizing 
Metatheory (Freiburg), in conjunction with {ICFP}},
  year =         {2007},
  month =        oct,
  address = {Freiburg},
  note = {(1 page abstract)},
}

@inproceedings{sarkar+:x86cc,
  author    = {Susmit Sarkar and
               Peter Sewell and
               Zappa Nardelli, Francesco and
               Scott Owens and
               Tom Ridge and
               Thomas Braibant and
               Magnus O. Myreen and
               Jade Alglave},
  title     = {The semantics of x86-CC multiprocessor machine code},
  booktitle = {Proceedings of {ACM} {SIGPLAN} Principles of Programming Languages ({POPL})},
  year      = {2009},
  pages     = {379--391},
  ee        = {http://doi.acm.org/10.1145/1480881.1480929},
}

@inproceedings{sewell+:ott-icfp,
  author    = {Peter Sewell and
               Zappa Nardelli, Francesco and
               Scott Owens and
               Gilles Peskine and
               Tom Ridge and
               Susmit Sarkar and
               Rok Strni\v{s}a},
  title     = {{Ott}: effective tool support for the working semanticist},
  booktitle = {{ACM} {SIGPLAN} International Conference on Functional Programming},
  year      = {2007},
  pages     = {1--12},
  ee        = {http://doi.acm.org/10.1145/1291151.1291155},
}

@article{sewell+:ott-jfp,
 author     = {Peter Sewell and 
               Zappa Nardelli, Francesco and 
               Scott Owens and 
               Gilles Peskine and 
               Thomas Ridge and 
               Susmit Sarkar and 
               Rok Strni\v{s}a},
 title      = {{Ott}: Effective Tool Support for the Working Semanticist},
 journal    = {Journal of Functional Programming},
 year       = {2010},
 volume     = {20},
 number     = {1},
 pages      = {70--122},
 month      = jan,
 ee         = {http://dx.doi.org/10.1017/S0956796809990293},
 note       = {Invited submission from ICFP 2007},
}

@inproceedings{zappanardelli+:rigorous-mm,
  author    = {Zappa Nardelli, Francesco and 
               Peter Sewell and 
               Jaroslav \v{S}ev\v{c}\'{\i}k and 
               Susmit Sarkar and 
               Scott Owens and 
               Luc Maranget and 
               Mark Batty and 
               Jade Alglave},
  title     = {Relaxed memory models must be rigorous},
  booktitle = {Proceedings of Exploiting Concurrency Efficiently and 
               Correctly -- ({EC})~${}^2$.  {CAV} 2009 Workshop}, 
  address   = {Grenoble, France},
  note      = {(4~page position paper)},
  year      = {2009},
  month     = jun,
}