Sites Inria

English version

Equipe de recherche MOSCOVA

Publications de l'équipe MOSCOVA

2012

Article dans des revues

titre
Fences in weak memory models (extended version)
auteur
Jade Alglave, Luc Maranget, Susmit Sarkar, Peter Sewell
article
Formal Methods in System Design, Springer Verlag, 2012, 40 (2), pp.170 - 205. <10.1007/s10703-011-0135-z>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01100778/file/fences-fmsd12.pdf BibTex

Communication dans un congrès

titre
An Axiomatic Memory Model for POWER Multiprocessors
auteur
Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian, Jade Alglave, Scott Owens, Rajeev Alur, Milo Martin, Peter Sewell, Derek Williams
article
Computer Aided Verification - 24th International Conference, CAV, Jul 2012, Berkely, United States. pp.495 - 512, 2012, <10.1007/978-3-642-31424-7_36>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01100773/file/cav12.pdf BibTex
titre
Synchronising C/C++ and POWER
auteur
Susmit Sarkar, Kayvan Memarian, Scott Owens, Mark Batty, Peter Sewell, Luc Maranget, Jade Alglave, Derek Williams
article
PLDI '12: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation, Jun 2012, Beijing, China. 2012, <10.1145/2254064.2254102>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01100798/file/top2.pdf BibTex

Thèse

titre
Types, compilers, and cryptography for secure distributed programming
auteur
Jeremy Planul
article
Programming Languages [cs.PL]. Ecole Polytechnique X, 2012. English
Accès au texte intégral et bibtex
https://pastel.archives-ouvertes.fr/pastel-00685356/file/these.pdf BibTex

2011

Communication dans un congrès

titre
Secure Distributed Programming with Value-dependent Types
auteur
Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang
article
16th ACM SIGPLAN International Conference on Functional Programming, Sep 2011, Tokyo, Japan. 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00596715/file/fstar-icfp-2011.pdf BibTex
titre
Stability in Weak Memory Models
auteur
Jade Alglave, Luc Maranget
article
CAV'11, Computer Aided Verification - 23rd International Conference, Jul 2011, Snowbird, United States. pp.50 - 66, 2011, <10.1007/978-3-642-22110-1_6>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01100806/file/cav11.pdf BibTex
titre
Understanding POWER multiprocessors
auteur
Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, Derek Williams
article
PLDI '11: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, Jun 2011, San Jose, United States. 2011, <10.1145/1993498.1993520>
Accès au bibtex
BibTex
titre
Litmus: Running Tests against Hardware
auteur
Luc Maranget, Jade Alglave, Susmit Sarkar, Peter Sewell
article
TACAS'11, 17th International Conference on Tools And Algorithms for the Construction and Analysis of Systems, Mar 2011, Saarbrücken, Germany. 2011, <10.1007/978-3-642-19835-9_5>
Accès au bibtex
BibTex

Pré-publication, Document de travail

titre
A Generic Formalised Framework for Reasoning About Weak Memory Models
auteur
Jade Alglave, Assia Mahboubi
article
2011
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00604656/file/itp.pdf BibTex

2010

Communication dans un congrès

titre
Fences in Weak Memory Models
auteur
Jade Alglave, Luc Maranget, Susmit Sarkar, Peter Sewell
article
CAV'10, Computer Aided Verification - 22nd International Conference, Jul 2010, Edinburgh, United Kingdom. 2010, <10.1007/978-3-642-14295-6_25>
Accès au bibtex
BibTex

2009

Communication dans un congrès

titre
A Relational Model of a Parallel and Non-deterministic lambda-Calculus
auteur
Thomas Ehrhard, Antonio Bucciarelli, Giulio Manzonetto
article
Sergei N. Artemov and Anil Nerode. Logical Foundations of Computer Science, International Symposium, LFCS 2009, Jan 2009, Deerfield Beach, FL, USA, France. Springer, 5407, pp.107-121, 2009, Lecture Notes in Computer Science
Accès au bibtex
BibTex

Rapport

titre
Fences in Weak Memory Models
auteur
Alglave Jade, Luc Maranget
article
[Research Report] RR-7010, INRIA. 2009
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00408568/file/RR-7010.pdf BibTex
titre
Fences and Synchronisation Idioms in Weak Memory Models
auteur
Jade Alglave, Luc Maranget
article
[Research Report] RR-7152, INRIA. 2009
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00440863/file/rr-7152.pdf BibTex
titre
Models and theories of lambda calculus
auteur
Giulio Manzonetto
article
[Research Report] 2009
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00380183/file/PhdShort.pdf BibTex

2008

Communication dans un congrès

titre
Abstraction of Clocks in Synchronous Data-flow Systems
auteur
Albert Cohen, Louis Mandel, Florence Plateau, Marc Pouzet
article
6th Asian Symposium on Programming Languages and Systems (APLAS), 2008, Unknown, Unknown or Invalid Region. 2008
Accès au bibtex
BibTex

2007

Communication dans un congrès

titre
Separation Logic for Small-step Cminor
auteur
Andrew W. Appel, Sandrine Blazy
article
Springer-Verlag. 20th Int. Conference on Theorem Proving in Higher Order Logics (TPHOLs 2007), Sep 2007, Kaiserslautern, Germany. 4732, pp.5-21, 2007, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00165915/file/paperTPHOL.pdf BibTex
titre
General Reversibility
auteur
Vincent Danos, Jean Krivine, Pawel Sobocinski
article
Jun 2007, Elsevier, pp.75-86, 2007, Electronic Notes in Theoretical Computer Science volume 175
Accès au bibtex
BibTex
titre
Executable Contracts for Incremental Prototypes of Embedded Systems
auteur
Lionel Morel, Louis Mandel
article
Formal Foundations of Embedded Software and Component-Based Software Architectures (FESCA), 2007, Portugal. pp.121-135, 2009
Accès au bibtex
BibTex
titre
A very modal model of a modern, major, general type system
auteur
Andrew W. Appel, Paul-André Melliès, Christopher D. Richards, Jérôme Vouillon
article
Annual Symposium on Principles of Programming Languages, 2007, Nice, France. ACM Press, pp.109-122, 2007, <10.1145/1190216.1190235>
Accès au bibtex
BibTex

Rapport

titre
Programming in JoCaml --- Extended Version
auteur
Louis Mandel, Luc Maranget
article
[Research Report] RR-6261, INRIA. 2007
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00166125/file/RR-6261.pdf BibTex
titre
Separation Logic for Small-step Cminor (extended version)
auteur
Andrew W. Appel, Sandrine Blazy
article
[Research Report] RR-6138, INRIA. 2007, pp.34
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00134699/file/sequential-rr.pdf BibTex

2006

Communication dans un congrès

titre
A list-machine benchmark for mechanized metatheory (extended abstract)
auteur
Andrew W. Appel, Xavier Leroy
article
Int. Workshop on Logical Frameworks and Meta-Languages (LFMTP 2006), Aug 2006, Seattle (Washington), United States. Elsevier, 174/5, pp.95-108, 2006, Electronic Notes in Theoretical Computer Science; Proceedings of the First International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2006). <10.1016/j.entcs.2007.01.020>
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00289543/file/listmachine-lfmtp.pdf BibTex

Rapport

titre
A list-machine benchmark for mechanized metatheory
auteur
Andrew W. Appel, Xavier Leroy
article
[Research Report] RR-5914, INRIA. 2006
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00077531/file/RR-5914.pdf BibTex
titre
A verification algorithm for Declarative Concurrent Programming
auteur
Jean Krivine
article
[Research Report] 2006
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00081218/file/RR-dcp.pdf BibTex

Thèse

titre
Security Properties in the lambda-calculus.
auteur
Tomasz Blanc
article
Cryptographie et sécurité [cs.CR]. Ecole Polytechnique X, 2006. Français
Accès au texte intégral et bibtex
https://pastel.archives-ouvertes.fr/pastel-00002090/file/Blanc.pdf BibTex

2005

Article dans des revues

titre
The Seal Calculus
auteur
Giuseppe Castagna, Jan Vitek, Francesco Zappa Nardelli
article
Information and Computation, Elsevier, 2005, 201 (1), pp.1-54
Accès au bibtex
BibTex

Communication dans un congrès

titre
Transactions in RCCS
auteur
Vincent Danos, Jean Krivine
article
Sixteenth International Conference on Concurrency Theory (CONCUR'05), 2005, United Kingdom. 3653, pp.398-412, 2005
Accès au bibtex
BibTex

Rapport

titre
Information Hiding, Inheritance and Concurrency
auteur
Qin Ma, Luc Maranget
article
[Research Report] RR-5631, INRIA. 2005, pp.74
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00070376/file/RR-5631.pdf BibTex

2004

Rapport

titre
Acute: High-level programming language design for distributed computation : Design rationale and language definition
auteur
Peter Sewell, James J. Leifer, Keith Wansbrough, Mair Allen-Williams, Francesco Zappa Nardelli, Pierre Habouzit, Viktor Vafeiadis
article
[Research Report] RR-5329, INRIA. 2004, pp.193
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00070671/file/RR-5329.pdf BibTex
titre
Behavioural Theory for Mobile Ambients
auteur
Massimo Merro, Francesco Zappa Nardelli
article
[Research Report] RR-5375, INRIA. 2004, pp.61
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00070628/file/RR-5375.pdf BibTex
titre
Compiling Pattern Matching in Join-Patterns
auteur
Qin Ma, Luc Maranget
article
[Research Report] RR-5160, INRIA. 2004
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00077047/file/RR-5160.pdf BibTex

2003

Communication dans un congrès

titre
Formal Molecular Biology done in CCS
auteur
Vincent Danos, Jean Krivine
article
BIO-CONCUR'03, Sep 2003, France. 180 (3), pp.31-49, 2007
Accès au bibtex
BibTex

Rapport

titre
Theorem Proving Modulo Revised Version
auteur
Gilles Dowek, Thérèse Hardin, Claude Kirchner
article
[Research Report] RR-4861, INRIA. 2003, pp.54
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00071722/file/RR-4861.pdf BibTex
titre
Global abstraction-safe marshalling with hash types
auteur
James J. Leifer, Gilles Peskine, Peter Sewell, Keith Wansbrough
article
[Research Report] RR-4851, INRIA. 2003
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00071732/file/RR-4851.pdf BibTex
titre
Expressive Synchronization Types for Inheritance in the Join Calculus
auteur
Qin Ma, Luc Maranget
article
[Research Report] RR-4889, INRIA. 2003
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00071693/file/RR-4889.pdf BibTex

2002

Rapport

titre
The M-calculus: a Higher-Order Distributed Process Calculus
auteur
Alan Schmitt, Jean-Bernard Stefani
article
[Research Report] RR-4361, INRIA. 2002
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00072227/file/RR-4361.pdf BibTex
titre
Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2
auteur
James J. Leifer
article
[Research Report] RR-4395, INRIA. 2002
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00072193/file/RR-4395.pdf BibTex
titre
Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 1
auteur
James J. Leifer
article
[Research Report] RR-4394, INRIA. 2002
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00072194/file/RR-4394.pdf BibTex

2001

Communication dans un congrès

titre
JOIN(X): Constraint-Based Type Inference for the Join-Calculus
auteur
Sylvain Conchon, François Pottier
article
David Sands. Proceedings of the 10th European Symposium on Programming (ESOP'01), Apr 2001, Genova, Springer Verlag, 2028, pp.221--236, 2001, Lecture notes in computer science
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00000029/file/conchon-fpottier-esop01.pdf BibTex

1999

Thèse

titre
Outils Génériques de Modélisation et de Démonstration pour la Formalisation des Mathématiques en Théorie des Types. Application à la Théorie des Catégories.
auteur
Amokrane Saibi
article
Autre [cs.OH]. Université Pierre et Marie Curie - Paris VI, 1999. Français
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00523810/file/Saibi_-_1999_-_Outils_GA_nA_riques_de_modA_lisation_et_de_dA_monstration_pour_la_Formalisation_des_MathA_matiques_en_thA_orie_des_Types_Application_A_la_thA_orie_des_catA_gories.pdf BibTex

Suivez Inria tout au long de son 50e anniversaire et au-delà !