@inproceedings{MadorHaimMSMAOAMSW:axiomatic-cav12,
title = {An Axiomatic Memory Model for {POWER} Multiprocessors},
author = {Mador-Haim, Sela and
          Luc Maranget and
          Susmit Sarkar and
          Kayvan Memarian and
          Jade Alglave and
          Scott Owens and
          Rajeev Alur and
          Milo Martin and
          Peter Sewell and
          Derek Williams},
booktitle = {Proceedings of the 24th International Conference on Computer Aided Verification {(CAV)}},
year = {2012},
month = jul,
note = {Forthcoming},
}

@inproceedings{SarkarMOBSMAW:synchronising-pldi12,
title = {Synchronising {C/C++} and {POWER}},
author = {Susmit Sarkar and
          Kayvan Memarian and
          Scott Owens and 
          Mark Batty and
          Peter Sewell and
          Luc Maranget and
          Jade Alglave and
          Derek Williams},
booktitle = {Proceedings of the 33rd {ACM} {SIGPLAN} Programming Language Design and Implementation (PLDI)},
conferenceloc = {Beijing, China},
conferencedate = {June 11--16, 2012},
year = {2012},
month = jun,
note = {Forthcoming},
}

@article{AlglaveMSS:fences-fmsd12,
  author    = {Jade Alglave and
               Luc Maranget and
               Susmit Sarkar and
               Peter Sewell},
  title     = {Fences in weak memory models (extended version)},
  journal   = {Formal Methods in System Design},
  volume    = {40},
  number    = {2},
  year      = {2012},
  month     = feb,
  pages     = {170--205},
  doi       = {10.1007/s10703-011-0135-z},
  issn      = {0925-9856},
  publisher = {Springer Netherlands},
}

@inproceedings{BattyMOSS:clarifying-popl12,
  author    = {Mark Batty and
               Kayvan Memarian and
               Scott Owens and
               Susmit Sarkar and
               Peter Sewell},
  title     = {Clarifying and compiling {C/C++} concurrency: from {C++11} to
               {POWER}},
  booktitle = {Proceedings of the 39th {ACM} {SIGPLAN}-{SIGACT} Symposium on
               Principles of Programming Languages {(POPL 2012)}},
  conferenceloc = {Philadelphia, Pennsylvania, USA}, 
  conferencedate = {January 22--28, 2012},
  year      = {2012},
  month     = jan,
  pages     = {509--520},
  doi       = {10.1145/2103656.2103717},
  editor    = {John Field and
               Michael Hicks},
  publisher = {{ACM} Press},
  isbn      = {978-1-4503-1083-3},
}

@inproceedings{BlanchetteWBOS:nitpick-ppdp11,
  author    = {Jasmin Christian Blanchette and
               Tjark Weber and
               Mark Batty and
               Scott Owens and
               Susmit Sarkar},
  title     = {Nitpicking {C++} concurrency},
  booktitle = {Proceedings of the 13th International {ACM} {SIGPLAN} Conference
               on Principles and Practice of Declarative Programming {(PPDP 2011)}}, 
  conferenceloc = {Odense, Denmark},
  conferencedate = {July 20--22, 2011}, 
  year      = {2011},
  month     = jul,
  pages     = {113--124},
  doi       = {10.1145/2003476.2003493},
  editor    = {Peter Schneider-Kamp and
               Michael Hanus},
  publisher = {{ACM} Press},
  isbn      = {978-1-4503-0776-5},
}

@inproceedings{SarkarSAMW:power-pldi11,
  author    = {Susmit Sarkar and
               Peter Sewell and
               Jade Alglave and
               Luc Maranget and
               Derek Williams},
  title     = {Understanding {POWER} multiprocessors},
  booktitle = {Proceedings of the 32nd {ACM} {SIGPLAN} Conference on Programming
               Language Design and Implementation {(PLDI 2011)}}, 
  conferenceloc = {San Jose, California, USA}, 
  conferencedate = {June 4--8, 2011},
  year      = {2011},
  month     = jun,
  pages     = {175--186},
  doi       = {10.1145/1993498.1993520},
  editor    = {Mary W. Hall and
               David A. Padua},
  publisher = {{ACM} Press},
  isbn      = {978-1-4503-0663-8},
}

@inproceedings{AlglaveMSS:litmus-tacas11,
  author    = {Jade Alglave and
               Luc Maranget and
               Susmit Sarkar and
               Peter Sewell},
  title     = {Litmus: Running Tests against Hardware},
  booktitle = {Proceedings of Tools and Algorithms for the Construction and Analysis of
               Systems - 17th International Conference {(TACAS 2011)}, Held
               as Part of the Joint European Conferences on Theory and
               Practice of Software {(ETAPS 2011)}}, 
  conferenceloc = {Saarbr{\"u}cken, Germany},
  conferencedate = {March 26--April 3, 2011},
  year      = {2011},
  month     = mar,
  pages     = {41--44},
  doi       = {10.1007/978-3-642-19835-9_5},
  editor    = {Parosh Aziz Abdulla and
               K. Rustan M. Leino},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6605},
  isbn      = {978-3-642-19834-2},
}

@inproceedings{BattyOSSW:c++-popl11,
  author    = {Mark Batty and
               Scott Owens and
               Susmit Sarkar and
               Peter Sewell and
               Tjark Weber},
  title     = {Mathematizing {C++} concurrency},
  booktitle = {Proceedings of the 38th {ACM} {SIGPLAN}-{SIGACT} Symposium on
               Principles of Programming Languages {(POPL 2011)}},
  conferenceloc = {Austin, Texas, USA},
  conferendedate = {January 26--28, 2011},
  year      = {2011},
  month     = jan,
  pages     = {55--66},
  doi       = {10.1145/1926385.1926394},
  editor    = {Thomas Ball and
               Mooly Sagiv},
  publisher = {{ACM} Press},
  isbn      = {978-1-4503-0490-0},
}

@techreport{BattyOSSW:c++-N3132,
  author = {Mark Batty and 
            Scott Owens and 
            Susmit Sarkar and 
            Peter Sewell and 
            Tjark Weber},
  title = {Mathematizing {C++} Concurrency: The Post-{Rapperswil} Model},
  institution = {ISO IEC JTC1/SC22/WG21},
  number = {N3132},
  year = 2010,
  month = aug,
  note = {\url{http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2010/n3132.pdf}},
}

@inproceedings{AlglaveMSS:fences-cav10,
  author    = {Jade Alglave and
               Luc Maranget and
               Susmit Sarkar and
               Peter Sewell},
  title     = {Fences in Weak Memory Models},
  booktitle = {Proceedings of Computer Aided Verification, 22nd International Conference
               {(CAV 2010)}}, 
  conferenceloc = {Edinburgh, UK}, 
  conferencedate = {July 15--19, 2010},
  year      = {2010},
  month     = jul,
  pages     = {258--272},
  doi       = {10.1007/978-3-642-14295-6_25},
  editor    = {Tayssir Touili and
               Byron Cook and
               Paul Jackson},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6174},
  isbn      = {978-3-642-14294-9},
}

@article{SewellSOZNM:x86tso-cacm10,
  author    = {Peter Sewell and
               Susmit Sarkar and
               Scott Owens and
               Zappa Nardelli, Francesco and
               Magnus O. Myreen},
  title     = {{x86-TSO}: a rigorous and usable programmer's model for x86
               multiprocessors},
  journal   = {Communications of the {ACM}},
  volume    = {53},
  number    = {7},
  year      = {2010},
  month     = jul,
  pages     = {89--97},
  issn      = {0001-0782},
  publisher = {{ACM}},
  address   = {New York, New York, USA},
  doi       = {10.1145/1785414.1785443},
}


@article{SewellZNOPRSS:ott-jfp10,
  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},
  volume    = {20},
  number    = {1},
  year      = {2010},
  month     = jan,
  pages     = {71--122},
  issn      = {0956-7968},
  publisher = {Cambridge University Press},
  doi       = {10.1017/S0956796809990293},
}

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

@inproceedings{OwensSS:x86tso-tphols09,
  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, 22nd International
               Conference {(TPHOLs 2009)}}, 
  conferenceloc = {Munich, Germany}, 
  conferendedate = {August 17--20, 2009},
  year      = {2009},
  month     = aug,
  pages     = {391--407},
  doi       = {10.1007/978-3-642-03359-9_27},
  editor    = {Stefan Berghofer and
               Tobias Nipkow and
               Christian Urban and
               Makarius Wenzel},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {5674},
  isbn      = {978-3-642-03358-2},
}

@inproceedings{ZappanardelliSSSOMBA:rigorousmm-ec209,
  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}, 
  conferenceloc = {Grenoble, France},
  note      = {(4~page position paper)},
  year      = {2009},
  month     = jun,
}

@inproceedings{AlglaveFIMSSZN:powerarm-damp09,
  author    = {Jade Alglave and
               Anthony C. J. 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},
  booktitle = {Proceedings of the {POPL} 2009 Workshop on Declarative Aspects
               of Multicore Programming {(DAMP 2009)}}, 
  conferenceloc = {Savannah, Georgia, USA},
  conferencedate = {January 20, 2009},
  year      = {2009},
  month     = jan,
  pages     = {13--24},
  doi       = {10.1145/1481839.1481842},
  editor    = {Leaf Petersen and
               Manuel M. T. Chakravarty},
  publisher = {{ACM} Press},
  isbn      = {978-1-60558-417-1},
}

@inproceedings{SarkarSZNORBMA09:x86cc-popl09,
  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 the 36th {ACM} {SIGPLAN}-{SIGACT} Symposium on
               Principles of Programming Languages {(POPL 2009)}}, 
  conferenceloc = {Savannah, Georgia, USA}, 
  conferencedate = {January 21--23, 2009},
  year      = {2009},
  month     = jan,
  pages     = {379--391},
  doi       = {10.1145/1480881.1480929},
  editor    = {Zhong Shao and
               Benjamin C. Pierce},
  publisher = {{ACM} Press},
  isbn      = {978-1-60558-379-2},
}

@phdthesis{Sarkar:phd,
 author = {Susmit Sarkar},
 title = {A Dependently Typed Programming Language, with applications
                  to Foundational Certified Code},
 month = may,
 year = 2009,
 school = {Carnegie Mellon University, School of Computer Science},
 address = {Pittsburgh, Pennsylvania},
}

@article{CraryS:mafcc-tocl08,
  author    = {Karl Crary and
               Susmit Sarkar},
  title     = {Foundational certified code in the {Twelf} metalogical framework},
  journal   = {{ACM} Transactions on Computational Logic {(TOCL)}},
  volume    = {9},
  number    = {3},
  year      = {2008},
  month     = jun,
  pages     = {16:1--16:26},
  issn      = {1529-3785},
  publisher = {{ACM}},
  address   = {New York, New York, USA},
  doi       = {10.1145/1352582.1352584},
}

@inproceedings{SarkarSZN:ottbinding-wmm07,
  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{SewellZNOPRSS:ott-icfp07,
  author    = {Peter Sewell and
               Zappa Nardelli, Francesco and
               Scott Owens and
               Gilles Peskine and
               Tom Ridge and
               Susmit Sarkar and
               Rok Strnisa},
  title     = {Ott: effective tool support for the working semanticist},
  booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference
               on Functional Programming {(ICFP 2007)}}, 
  conferenceloc = {Freiburg, Germany},
  conferencedate = {October 1--3, 2007},
  year      = {2007},
  month     = oct,
  pages     = {1--12},
  doi       = {10.1145/1291151.1291155},
  editor    = {Ralf Hinze and
               Norman Ramsey},
  publisher = {{ACM} Press},
  isbn      = {978-1-59593-815-2},
}

@inproceedings{SarkarPC:oracle-iclp05,
  author    = {Susmit Sarkar and
               Brigitte Pientka and
               Karl Crary},
  title     = {Small Proof Witnesses for {LF}},
  booktitle = {Proceedings of Logic Programming, 21st International Conference {(ICLP 2005)}},
  conferenceloc = {Sitges, Spain},
  conferencedate = {October 2--5, 2005},
  year      = {2005},
  month     = oct,
  pages     = {387--401},
  doi       = {10.1007/11562931_29},
  editor    = {Maurizio Gabbrielli and
               Gopal Gupta},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {3668},
  year      = {2005},
  isbn      = {3-540-29208-X},
}

@techreport{CraryS:mafcc-tr,
  author = {Karl Crary and Susmit Sarkar},
  title = {Foundational certified code in a metalogical framework},
  institution = {Carnegie Mellon University, School of Computer Science},
  year = 2003,
  number = {CMU-CS-03-108},
}

@inproceedings{CraryS:mafcc-cade03,
  author    = {Karl Crary and
               Susmit Sarkar},
  title     = {Foundational Certified Code in a Metalogical Framework},
  booktitle = {Proceedings of Automated Deduction - CADE-19, 19th International Conference
               on Automated Deduction},
  conferenceloc = {Miami Beach, Florida, USA}, 
  conferencedate = {July 28 -- August 2, 2003},
  year      = {2003},
  month     = jul,
  pages     = {106--120},
  doi       = {10.1007/978-3-540-45085-6_9},
  editor    = {Franz Baader},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {2741},
  year      = {2003},
  isbn      = {3-540-40559-3},
}

@techreport{AshwinGSJS:image-tr,
  author = {Ashwin T.V.  and 
            Sugata Ghosal and 
            Abhinanda Sarkar and 
            Navendu Jain and 
            Susmit Sarkar},
  title = {Robust Non-parametric Relevance Feedback for Image Retrieval},
  institution = {{IBM} India Research Laboratory},
  year = 2001,
  month = dec,
  number = {},
}