- Présentation
- Publications HAL
- Rapports d'activité
Equipe de recherche MOSCOVA
Publications de l'équipe MOSCOVA
2012
Thèses
- Titre
- Typage, compilation, et cryptographie pour la programmation repartie securisée
- Auteurs
- Jeremy Planul

- Détail
- Ecole Polytechnique X, Feb. 2012. English
- Accès au texte intégral et bibtex
-
2011
Communications avec actes
- Titre
- Secure Distributed Programming with Value-dependent Types
- Auteurs
- Nikhil Swamy; Juan Chen; Cédric Fournet; Pierre-Yves Strub; Karthikeyan Bhargavan; Jean Yang
- Détail
- 16th ACM SIGPLAN International Conference on Functional Programming, Sep 2011, Tokyo, Japan.
- Accès au texte intégral et bibtex
-
Documents sans référence de publication
- Titre
- A Generic Formalised Framework for Reasoning About Weak Memory Models
- Auteurs
- Jade Alglave; Assia Mahboubi
- Détail
- Jun. 2011
- Accès au texte intégral et bibtex
-
2009
Communications avec actes
- Titre
- Executable Contracts for Incremental Prototypes of Embedded Systems
- Auteurs
- Lionel Morel; Louis Mandel
- Détail
- Formal Foundations of Embedded Software and Component-Based Software Architectures (FESCA), 2007, Portugal. pp. 121-135, 2009
- Accès au bibtex
-
- Titre
- A Relational Model of a Parallel and Non-deterministic lambda-Calculus
- Auteurs
- Thomas Ehrhard; Antonio Bucciarelli; Giulio Manzonetto
- Détail
- 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, Lecture Notes in Computer Science
- Accès au bibtex
-
Rapports
- Titre
- Models and theories of lambda calculus
- Auteurs
- Giulio Manzonetto
- Détail
- [Research Report], 2009
- Accès au texte intégral et bibtex
-
- Titre
- Fences in Weak Memory Models
- Auteurs
- Alglave Jade; Luc Maranget
- Détail
- [Research Report], 2009. RR-7010
- Accès au texte intégral et bibtex
-
- Titre
- Fences and Synchronisation Idioms in Weak Memory Models
- Auteurs
- Jade Alglave; Luc Maranget
- Détail
- [Research Report], 2009. RR-7152
- Accès au texte intégral et bibtex
-
2007
Communications avec actes
- Titre
- General Reversibility
- Auteurs
- Vincent Danos; Jean Krivine; Pawel Sobocinski
- Détail
- Jun 2007. Elsevier, pp. 75-86, Electronic Notes in Theoretical Computer Science volume 175
- Accès au bibtex
-
- Titre
- A very modal model of a modern, major, general type system
- Auteurs
- Andrew W. Appel; paul-andré melliès; Christopher D. Richards; Jérôme Vouillon
- Détail
- Annual Symposium on Principles of Programming Languages, 2007, Nice, France. ACM Press, pp. 109-122
- Accès au bibtex
-
- Titre
- Formal Molecular Biology done in CCS
- Auteurs
- Vincent Danos; Jean Krivine
- Détail
- BIO-CONCUR'03, Sep 2003, France. 180, pp. 31-49, 2007
- Accès au bibtex
-
- Titre
- Separation Logic for Small-step Cminor
- Auteurs
- Andrew W. Appel; Sandrine Blazy
- Détail
- Springer-Verlag. 20th Int. Conference on Theorem Proving in Higher Order Logics (TPHOLs 2007), Sep 2007, Kaiserslautern, Germany. 4732, pp. 5-21, Lecture Notes in Computer Science
- Accès au texte intégral et bibtex
-
Rapports
- Titre
- Separation Logic for Small-step Cminor (extended version)
- Auteurs
- Andrew W. Appel; Sandrine Blazy
- Détail
- [Research Report], 2007, pp. 34. RR-6138
- Accès au texte intégral et bibtex
-
- Titre
- Programming in JoCaml --- Extended Version
- Auteurs
- Louis Mandel; Luc Maranget
- Détail
- [Research Report], 2007. RR-6261
- Accès au texte intégral et bibtex
-
2006
Communications avec actes
- Titre
- A list-machine benchmark for mechanized metatheory (extended abstract)
- Auteurs
- Andrew W. Appel; Xavier Leroy
- Détail
- Int. Workshop on Logical Frameworks and Meta-Languages (LFMTP 2006), Aug 2006, Seattle (Washington), United States. Elsevier, Proceedings of the First International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2006), 174/5, pp. 95-108, Electronic Notes in Theoretical Computer Science
- Accès au texte intégral et bibtex
-
Rapports
- Titre
- A list-machine benchmark for mechanized metatheory
- Auteurs
- Andrew W. Appel; Xavier Leroy
- Détail
- [Research Report], 2006. RR-5914
- Accès au texte intégral et bibtex
-
- Titre
- A verification algorithm for Declarative Concurrent Programming
- Auteurs
- Jean Krivine
- Détail
- [Research Report], 2006
- Accès au texte intégral et bibtex
-
Thèses
- Titre
- Propriétés de sécurité dans le lambda-calcul.
- Auteurs
- Tomasz Blanc
- Détail
- Ecole Polytechnique X, Nov. 2006. French
- Accès au texte intégral et bibtex
-
2005
Articles dans des revues avec comité de lecture
- Titre
- The Seal Calculus
- Auteurs
- Giuseppe Castagna; Jan Vitek; Francesco Zappa Nardelli
- Détail
- Information and Computation, 2005, 201 (1), pp. 1-54
- Accès au bibtex
-
Communications avec actes
- Titre
- Transactions in RCCS
- Auteurs
- Vincent Danos; Jean Krivine
- Détail
- Sixteenth International Conference on Concurrency Theory (CONCUR'05), 2005, United Kingdom. 3653, pp. 398-412
- Accès au bibtex
-
Rapports
- Titre
- Information Hiding, Inheritance and Concurrency
- Auteurs
- Qin Ma; Luc Maranget
- Détail
- [Research Report], 2005, pp. 74. RR-5631
- Accès au texte intégral et bibtex
-
2004
Rapports
- Titre
- Behavioural Theory for Mobile Ambients
- Auteurs
- Massimo Merro; Francesco Zappa Nardelli
- Détail
- [Research Report], 2004, pp. 61. RR-5375
- Accès au texte intégral et bibtex
-
- Titre
- Acute: High-level programming language design for distributed computation : Design rationale and language definition
- Auteurs
- Peter Sewell; James J. Leifer; Keith Wansbrough; Mair Allen-Williams; Francesco Zappa Nardelli; Pierre Habouzit; Viktor Vafeiadis
- Détail
- [Research Report], 2004, pp. 193. RR-5329
- Accès au texte intégral et bibtex
-
- Titre
- Compiling Pattern Matching in Join-Patterns
- Auteurs
- Qin Ma; Luc Maranget
- Détail
- [Research Report], 2004. RR-5160
- Accès au texte intégral et bibtex
-
2003
Rapports
- Titre
- Expressive Synchronization Types for Inheritance in the Join Calculus
- Auteurs
- Qin Ma; Luc Maranget
- Détail
- [Research Report], 2003. RR-4889
- Accès au texte intégral et bibtex
-
- Titre
- Theorem Proving Modulo Revised Version
- Auteurs
- Gilles Dowek; Thérèse Hardin; Claude Kirchner
- Détail
- [Research Report], 2003, pp. 54. RR-4861
- Accès au texte intégral et bibtex
-
- Titre
- Global abstraction-safe marshalling with hash types
- Auteurs
- James J. Leifer; Gilles Peskine; Peter Sewell; Keith Wansbrough
- Détail
- [Research Report], 2003. RR-4851
- Accès au texte intégral et bibtex
-
2002
Rapports
- Titre
- Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2
- Auteurs
- James J. Leifer
- Détail
- [Research Report], 2002. RR-4395
- Accès au texte intégral et bibtex
-
- Titre
- Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 1
- Auteurs
- James J. Leifer
- Détail
- [Research Report], 2002. RR-4394
- Accès au texte intégral et bibtex
-
- Titre
- The M-calculus: a Higher-Order Distributed Process Calculus
- Auteurs
- Alan Schmitt; Jean-Bernard Stefani
- Détail
- [Research Report], 2002. RR-4361
- Accès au texte intégral et bibtex
-
2001
Communications avec actes
- Titre
- JOIN(X): Constraint-Based Type Inference for the Join-Calculus
- Auteurs
- Sylvain Conchon; François Pottier
- Détail
- David Sands. Proceedings of the 10th European Symposium on Programming (ESOP'01), Apr 2001, Genova. Springer Verlag, Lecture notes in computer science, 2028, pp. 221-236
- Accès au texte intégral et bibtex
-
1999
Thèses
- 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.
- Auteurs
- Amokrane Saibi
- Détail
- Université Pierre et Marie Curie - Paris VI, Mar. 1999. French
- Accès au texte intégral et bibtex
-
Archives
En savoir plus
Retrouvez toutes les publications scientifiques de nos équipes de recherche sur HAL Inria
Inria
Inria.fr
Inria Channel

Voir aussi