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 url
Détail
Ecole Polytechnique X, Feb. 2012. English
Accès au texte intégral et bibtex
these.pdf 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
fstar-icfp-2011.pdf 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
itp.pdf 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
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
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
PhdShort.pdf PhdShort.ps 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
RR-7010.pdf RR-7010.ps 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
rr-7152.pdf 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
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
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
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
paperTPHOL.pdf paperTPHOL.ps 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
sequential-rr.pdf sequential-rr.ps 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
RR-6261.pdf 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
listmachine-lfmtp.pdf 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
RR-5914.pdf RR-5914.ps 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
RR-dcp.pdf RR-dcp.ps 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
Blanc.pdf 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
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
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
RR-5631.pdf RR-5631.ps 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
RR-5375.pdf RR-5375.ps 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
RR-5329.pdf RR-5329.ps 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
RR-5160.pdf RR-5160.ps 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
RR-4889.pdf RR-4889.ps 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
RR-4861.pdf RR-4861.ps 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
RR-4851.pdf RR-4851.ps 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
RR-4395.pdf RR-4395.ps 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
RR-4394.pdf RR-4394.ps 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
RR-4361.pdf RR-4361.ps 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
conchon-fpottier-esop01.pdf conchon-fpottier-esop01.ps 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
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