Sites Inria

Equipe de recherche PI.R2

Publications de l'équipe PI.R2

2014

Communication dans un congrès

titre
Universe Polymorphism in Coq
auteur
Matthieu Sozeau, Nicolas Tabareau
article
Interactive Theorem Proving, Jul 2014, Vienna, Austria
Accès au bibtex
BibTex
titre
The duality of construction
auteur
Paul Downen, Zena Ariola
article
ESOP 2014 : European Symposium on Programming, Apr 2014, Grenoble, France. 15 p
Accès au bibtex
BibTex
titre
Models of a Non-Associative Composition
auteur
Guillaume Munch-Maccagnoni
article
Anca Muscholl. FOSSACS 2014 - 17th International Conference on Foundations of Software Science and Computation Structures, Apr 2014, Grenoble, France. Springer, 8412, pp.396-410, Lecture Notes in Computer Science; Foundations of Software Science and Computation Structures. 10.1007/978-3-642-54830-7_26
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00996729/file/duploids.pdf BibTex

Thèse

titre
De nouveaux outils pour calculer avec des inductifs en Coq
auteur
Pierre Boutillier
article
Programming Languages. Université Paris-Diderot - Paris VII, 2014. French
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-01054723/file/these_boutillier.pdf BibTex

Pré-publication, Document de travail

titre
Polygraphs of finite derivation type
auteur
Yves Guiraud, Philippe Malbos
article
46 pages. 2014
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00932845/file/ihdr.pdf BibTex
titre
Coherent presentations of Artin monoids
auteur
Stéphane Gaussent, Yves Guiraud, Philippe Malbos
article
45 pages. 2014
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00682233/file/polycox.pdf BibTex
titre
Linear polygraphs and Koszulity of algebras
auteur
Yves Guiraud, Eric Hoffbeck, Philippe Malbos
article
2014
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01006220/file/groebnerAH.pdf BibTex

2013

Article dans des revues

titre
Certifying and reasoning about cost annotations of functional programs
auteur
Roberto M. Amadio, Yann Régis-Gianas
article
Higher-Order and Symbolic Computation, Springer Verlag (Germany), 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00629473/file/main.pdf BibTex

Communication dans un congrès

titre
A Homotopical Completion Procedure with Applications to Coherence of Monoids
auteur
Yves Guiraud, Philippe Malbos, Samuel Mimram
article
Van Raamsdonk, Femke. RTA - 24th International Conference on Rewriting Techniques and Applications - 2013, Jun 2013, Eindhoven, Netherlands. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 21, pp.223-238, Leibniz International Proceedings in Informatics (LIPIcs). 10.4230/LIPIcs.RTA.2013.223
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00818253/file/rta13FinalLong.pdf BibTex
titre
Lightweight proof by reflection using a posteriori simulation of effectful computation
auteur
Guillaume Claret, Lourdes Del Carmen Gonzalez Huesca, Yann Régis-Gianas, Beta Ziliani
article
Interactive Theorem Proving, Jul 2013, Rennes, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00870110/file/simulation-based-pbr-final.pdf BibTex
titre
Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems
auteur
Bruno Barras, Lourdes Del Carmen Gonzalez Huesca, Hugo Herbelin, Yann Régis-Gianas, Enrico Tassi, Makarius Wenzel, Burkhart Wolff
article
MKM/Calculemus/DML, Jul 2013, Bath, United Kingdom. pp.359-363
Accès au bibtex
BibTex
titre
Un régime au concentré d'automate
auteur
Pierre-Marie Pédrot
article
Damien Pous and Christine Tasson. JFLA - Journées francophones des langages applicatifs, Feb 2013, Aussois, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00779752/file/jfla2013-10.pdf BibTex

Chapitre d'ouvrage

titre
Identities among relations for higher-dimensional rewriting systems
auteur
Yves Guiraud, Philippe Malbos
article
Operads 2009, 26, Société Mathématique de France, pp.145-161, 2013, Séminaires et Congrès
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00426228/file/niar.pdf BibTex

Ouvrage (y compris édition critique et traduction)

titre
Homotopy Type Theory: Univalent Foundations of Mathematics
auteur
Peter Aczel, Benedikt Ahrens, Thorsten Altenkirch, Steve Awodey, Bruno Barras, Andrej Bauer, Yves Bertot, Marc Bezem, Thierry Coquand, Eric Finster, Daniel Grayson, Hugo Herbelin, André Joyal, Dan Licata, Peter Lumsdaine, Assia Mahboubi, Per Martin-Löf, Sergey Melikhov, Alvaro Pelayo, Andrew Polonsky, Michael Shulman, Matthieu Sozeau, Bas Spitters, Benno Van Den Berg, Vladimir Voevodsky, Michael Warren, Carlo Angiuli, Anthony Bordg, Guillaume Brunerie, Chris Kapulkin, Egbert Rijke, Kristina Sojakova, Jeremy Avigad, Cyril Cohen, Robert Constable, Pierre-Louis Curien, Peter Dybjer, Martín Escardó, Kuen-Bang Hou, Nicola Gambino, Richard Garner, Georges Gonthier, Thomas Hales, Robert Harper, Martin Hofmann, Pieter Hofstra, Joachim Koch, Nicolai Kraus, Nuo Li, Zhaohui Luo, Michael Nahas, Erik Palmgren, Emily Riehl, Dana Scott, Philip Scott, Sergei Soloviev
article
Aucun, pp.448, 2013
Accès au bibtex
BibTex

Thèse

titre
Syntax and Models of a non-Associative Composition of Programs and Proofs
auteur
Guillaume Munch-Maccagnoni
article
Logic in Computer Science. Université Paris-Diderot - Paris VII, 2013. English
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00918642/file/these-screen-final.pdf BibTex

Pré-publication, Document de travail

titre
Simple simpl
auteur
Pierre Boutillier
article
2013
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00816918/file/ITP13_Boutillier.pdf BibTex
titre
A dependently-typed construction of semi-simplicial types
auteur
Hugo Herbelin
article
2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00935446/file/simplicial-revise-final.pdf BibTex
titre
Univalence for free
auteur
Matthieu Sozeau, Nicolas Tabareau
article
2013
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00786589/file/main.pdf BibTex

2012

Article dans des revues

titre
Partiality and Recursion in Interactive Theorem Provers - An Overview
auteur
Ana Bove, Alexander Krauss, Matthieu Sozeau
article
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2012
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00691459/file/main.pdf BibTex
titre
Continuation-passing Style Models Complete for Intuitionistic Logic
auteur
Danko Ilik
article
Annals of Pure and Applied Logic, Elsevier Masson, 2012, 10.1016/j.apal.2012.05.003
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00647390/file/intcomp.pdf BibTex
titre
Pure Type System conversion is always typable
auteur
Vincent Siles, Hugo Herbelin
article
Journal of Functional Programming, Cambridge University Press (CUP), 2012, 22 (2), pp.153 - 180. 10.1017/S0956796812000044
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00497177/file/PTSATR.pdf BibTex
titre
Böhm theorem and Böhm trees for the Lambda-mu-calculus
auteur
Alexis Saurin
article
Theoretical Computer Science, Elsevier, 2012, 435, pp.106-138. 10.1016/j.tcs.2012.02.027
Accès au bibtex
BibTex
titre
Delimited control operators prove Double-negation Shift
auteur
Danko Ilik
article
Annals of Pure and Applied Logic, Elsevier Masson, 2012, Kurt Goedel Research Prize Fellowships 2010, 163 (11), pp.1549-1559. 10.1016/j.apal.2011.12.008
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00647389/file/article.pdf BibTex
titre
Higher-dimensional normalisation strategies for acyclicity
auteur
Yves Guiraud, Philippe Malbos
article
Advances in Mathematics, Elsevier, 2012, 231 (3-4), pp.2294-2351. 10.1016/j.aim.2012.05.010
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00531242/file/ktheory.pdf BibTex
titre
Coherence in monoidal track categories
auteur
Yves Guiraud, Philippe Malbos
article
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2012, 22 (6), pp.931-969
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00470795/file/cohe.pdf BibTex

Communication dans un congrès

titre
Safe Incremental Type Checking
auteur
Matthias Puech, Yann Régis-Gianas
article
TLDI 2012 - Seventh ACM SIGPLAN Workshop on Types in Language Design and Implementation, Jan 2012, Philadelphia, United States
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00650341/file/abstract.pdf BibTex
titre
Certifying and reasoning on cost annotations in C programs
auteur
Nicolas Ayache, Roberto Amadio, Yann Régis-Gianas
article
FMICS 2012 - 17th International Workshop on Formal Methods for Industrial Critical Systems, Aug 2012, Paris, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00702665/file/ccac-fmics-final.pdf BibTex
titre
A Constructive Proof of Dependent Choice, Compatible with Classical Logic
auteur
Hugo Herbelin
article
LICS 2012 - 27th Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2012, Dubrovnik, Croatia. IEEE Computer Society, pp.365-374, Proceedings of the 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, 25-28 June 2012, Dubrovnik, Croatia
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00697240/file/Herbelin-lics12.pdf BibTex
titre
Extending Type Theory with Forcing
auteur
Guilhem Jaber, Nicolas Tabareau, Matthieu Sozeau
article
LICS 2012 : Logic In Computer Science, Jun 2012, Dubrovnik, Croatia. pp.0-0
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00685150/file/forcing_lics.pdf BibTex
titre
Classical call-by-need sequent calculi : The unity of semantic artifacts
auteur
Zena Ariola, Paul Downen, Hugo Herbelin, Keiko Nakata, Alexis Saurin
article
Tom Schrijvers and Peter Thiemann. FLOPS 2012 - 11th International Symposium on Functional and Logic Programming, May 2012, Kobe, Japan. Springer, 7294, pp.32-46, Lecture Notes in Computer Science; Functional and Logic Programming - 11th International Symposium, FLOPS 2012, Kobe, Japan, May 23-25, 2012. Proceedings. 10.1007/978-3-642-29822-6
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00697241/file/classical-need-artifacts.pdf BibTex
titre
A relaxation of Coq's guard condition
auteur
Pierre Boutillier
article
JFLA - Journées Francophones des langages applicatifs - 2012, Feb 2012, Carnac, France. pp.1 - 14
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00651780/file/boutillier.pdf BibTex
titre
Coq avec Classes
auteur
Matthieu Sozeau
article
JFLA - Journées Françaises des Langages Applicatifs, Feb 2012, Carnac, France
Accès au bibtex
BibTex

Autre publication

titre
A gentle introduction to type classes and relations in Coq
auteur
Pierre Castéran, Matthieu Sozeau
article
This document presents the main features of type classes and user-defined relations in the Coq pr.. 2012
Accès au bibtex
BibTex
titre
Forcing in Coq
auteur
Matthieu Sozeau, Nicolas Tabareau, Guilhem Jaber
article
A plugin for Coq that implements a generic Forcing translation for any given set of conditions. I.. 2012
Accès au bibtex
BibTex

Rapport

titre
Eliminating Skolem Functions in Peano Arithmetic with Interactive Realizability
auteur
Federico Aschieri, Margherita Zorzi
article
[Technical Report] 2012
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00690270/file/ConservativeSKFull.pdf BibTex
titre
Interactive Realizability for Classical Peano Arithmetic with Skolem Axioms
auteur
Federico Aschieri
article
[Technical Report] 2012
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00685360/file/RealizabilityPAfull.pdf BibTex

Pré-publication, Document de travail

titre
Interactive Realizability for Second-Order Heyting Arithmetic with EM1 and SK1
auteur
Federico Aschieri
article
2012
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00657054/file/RealizersHASEM1final.pdf BibTex

2011

Article dans des revues

titre
Preface to Girard's Festschrift
auteur
Pierre-Louis Curien
article
Theoretical Computer Science, Elsevier, 2011, 412 (20), pp.1853-1859
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00551737/file/girard-preface.pdf BibTex

Communication dans un congrès

titre
Classical Call-by-need and duality
auteur
Zena Ariola, Hugo Herbelin, Alexis Saurin
article
C.-H. Luke Ong. TLCA 2011 - Typed Lambda Calculi and Applications, Jun 2011, Novi Sad, Serbia. Springer, 6690, pp.27-44, Lecture Notes in Computer Science; Typed Lambda Calculi and Applications - 10th International Conference. 10.1007/978-3-642-21691-6_6
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00630156/file/tlca.pdf BibTex

2010

Article dans des revues

titre
Kripke Models for Classical Logic
auteur
Danko Ilik, Gyesik Lee, Hugo Herbelin
article
Annals of Pure and Applied Logic, Elsevier Masson, 2010, Special Issue: Classical Logic and Computation (2008), 161 (11), pp.1367-1378. 10.1016/j.apal.2010.04.007
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00371959/file/classical_kripke_rev3.pdf BibTex
titre
Proof and Refutation in MALL as a game
auteur
Olivier Delande, Dale Miller, Alexis Saurin
article
Annals of Pure and Applied Logic, Elsevier Masson, 2010, 161 (5), pp.654-672. 10.1016/j.apal.2009.07.017
Accès au bibtex
BibTex
titre
Typing streams in the $\Lambda\mu$-calculus
auteur
Alexis Saurin
article
ACM Transactions on Computational Logic, Association for Computing Machinery (ACM), 2010, 11 (4), pp.28-61. 10.1145/1805950.1805958
Accès au bibtex
BibTex

Communication dans un congrès

titre
An intuitionistic logic that proves Markov's principle
auteur
Hugo Herbelin
article
Logic In Computer Science, Jul 2010, Edinburgh, United Kingdom. IEEE Computer Society, pp.50-56, Proceedings, 25th Annual IEEE Symposium on Logic in Computer Science (LICS '10), Edinburgh, UK, 11-14 July 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00481815/file/herbelin.LICS2010.pdf BibTex
titre
Equality is typable in Semi-Full Pure Type Systems
auteur
Vincent Siles, Hugo Herbelin
article
Logic In Computer Science - LICS 2010, Jul 2010, Edinburgh, United Kingdom. 10 p
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00496988/file/herbelin.siles.LICS2010.pdf BibTex
titre
Polarity and the Logic of Delimited Continuations
auteur
Noam Zeilberger
article
25th Annual IEEE Symposium on Logic in Computer Science (LICS 2010), Jul 2010, Edinburgh, United Kingdom. pp.219 - 227, 10.1109/LICS.2010.23
Accès au bibtex
BibTex
titre
Towards typed repositories of proofs
auteur
Matthias Puech, Yann Regis-Gianas
article
Mathematically Intelligent Proof Search - MIPS 2010, Jul 2010, Paris, France
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00525874/file/puech-regis-gianas-mips-2010.pdf BibTex
titre
From Focalization of Logic to the Logic of Focalization
auteur
Michele Basaldella, Alexis Saurin, Kazushige Terui
article
Twenty-Sixth Conference on the Mathematical Foundations of Programming Semantics - MFPS XXVI, May 2010, Ottawa, Canada. pp.161-176, Electronic Notes Theoretical Computer Science. 10.1016/j.entcs.2010.08.010
Accès au bibtex
BibTex
titre
Operads, clones, and distributive laws
auteur
Pierre-Louis Curien
article
Chengming Bai, Li Guo and Jean-Louis Loday. Operads and Universal Algebra : Proceedings of China-France Summer Conference, Jul 2010, Tianjin, China. World Scientific, pp.25-50, Nankai Series in Pure, Applied Mathematics and Theoretical Physics, Vol. 9
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00697065/file/Operads-PLC.pdf BibTex
titre
Standardization and Böhm Trees for $\Lambda\mu$-Calculus
auteur
Alexis Saurin
article
Tenth International Symposium on Functional and Logic Programming - FLOPS 2010, Apr 2010, Sendai, Japan. Springer, 6009, pp.134-149, Lecture notes in computer science. 10.1007/978-3-642-12251-4_11
Accès au bibtex
BibTex
titre
Elaborations in Type Theory
auteur
Matthieu Sozeau
article
DTP'10 - Dependently Typed Programming - 2010, Jul 2010, Edinburgh, United Kingdom
Accès au bibtex
BibTex
titre
The duality of computation under focus
auteur
Pierre-Louis Curien, Guillaume Munch-Maccagnoni
article
IFIP International Conference on Theoretical Computer Science, Sep 2010, Brisbane, Australia. Springer Verlag, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00491236/file/TCS-2010.pdf BibTex
titre
A Hierarchy for Delimited Continuations in Call-by-Name
auteur
Alexis Saurin
article
13th International Conference on Software Science and Computational Structures - FOSSACS 2010, Mar 2010, Paphos, Cyprus. Springer, 6014, pp.374-388, Lecture notes in computer science. 10.1007/978-3-642-12032-9_26
Accès au bibtex
BibTex

Chapitre d'ouvrage

titre
The Duality of Computation under Focus
auteur
Pierre-Louis Curien, Guillaume Munch-Maccagnoni
article
Cristian S. Calude; Vladimiro Sassone. Theoretical Computer Science, 323, Springer, pp.165-181, 2010, IFIP Advances in Information and Communication Technology, 978-3-642-15239-9. 10.1007/978-3-642-15240-5_13
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01054461/file/03230167.pdf BibTex

Rapport

titre
Certifying cost annotations in compilers
auteur
Roberto M. Amadio, Nicolas Ayache, Yann Régis-Gianas, Ronan Saillard
article
2010
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00524715/file/ccac-hal.pdf BibTex

Thèse

titre
Développement modulaire de théories et gestion de l'espace de nom pour l'assistant de preuve Coq.
auteur
Elie Soubiran
article
Programming Languages. Ecole Polytechnique X, 2010. French
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00679201/file/these.pdf BibTex
titre
Investigation on the typing of equality in type systems
auteur
Vincent Siles
article
Logic in Computer Science. Ecole Polytechnique X, 2010. English
Accès au texte intégral et bibtex
https://pastel.archives-ouvertes.fr/pastel-00556578/file/these.pdf BibTex
titre
Constructive Completeness Proofs and Delimited Control
auteur
Danko Ilik
article
Software Engineering. Ecole Polytechnique X, 2010. English
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00529021/file/thesis-danko-ilik.pdf BibTex

2009

Communication dans un congrès

titre
On the Meaning of Focalization
auteur
Alexis Saurin, Michele Basaldella, Kazushige Terui
article
Lecomte and Tronçon. workshop on Games, Dialog and Interaction, Sep 2009, Paris, France. Springer-Verlag, 6505, pp.78-87, LNAI
Accès au bibtex
BibTex
titre
Forcing-based cut-elimination for Gentzen-style intuitionistic sequent calculus
auteur
Hugo Herbelin, Gyesik Lee
article
Hiroakira Ono and Makoto Kanazama and Ruy de Queiroz. Workshop on Logic, Language, Information and Computation, Jun 2009, Tokyo, Japan. Springer, 5514, pp.209-217, Lecture Notes in Artificial Intelligence; Logic, Language, Information and Computation, 16th International Workshop, WoLLIC 2009, Tokyo, Japan, June 21-25, 2009, Proceedings
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00381554/file/wollic-HerLee09-kripke-cut-elim.pdf BibTex
titre
An Operational Account of Call-By-Value Minimal and Classical $\lambda$-calculus in ''Natural Deduction'' Form
auteur
Hugo Herbelin, Stéphane Zimmermann
article
Pierre-Louis Curien. TLCA 2009 - 9th International Conference on Typed Lambda-Calculi and Applications, Jul 2009, Brasilia, Brazil. Springer-Verlag, 5608, pp.142-156, Lecture Notes in Computer Science; Typed Lambda Calculi and Applications. 10.1007/978-3-642-02273-9_12
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00389903/file/ndcbv.pdf BibTex
titre
Focalisation and Classical Realisability (version with appendices)
auteur
Guillaume Munch-Maccagnoni
article
Erich Grädel and Reinhard Kahle. 18th EACSL Annual Conference on Computer Science Logic - CSL 09, Sep 2009, Coimbra, Portugal. Springer-Verlag, 5771, pp.409-423, Lecture notes in computer science. 10.1007/978-3-642-04027-6_30
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00409793/file/focalisation_and_classical_realisability_long.pdf BibTex

Chapitre d'ouvrage

titre
Sequential algorithms as bistable maps
auteur
Pierre-Louis Curien
article
Yves Bertot, Gérard Huet, Jean-Jacques Lévy and Gordon Plotkin. From semantics to computer science: essays in honour of Gilles Kahn, Cambridge University Press, pp.51-71, 2009
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00155296/file/laird-sa.pdf BibTex

Ouvrage (y compris édition critique et traduction)

titre
Introduction to ''Interactive models of computation and program behaviour
auteur
Pierre-Louis Curien
article
Société Mathématique de France, pp.xi-xv, 2009, Panoramas et Synthèses
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00697119/file/intro-pano.pdf BibTex

Pré-publication, Document de travail

titre
λμ-calculus and Λμ-calculus: a Capital Difference
auteur
Hugo Herbelin, Alexis Saurin
article
2009
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00524942/file/apal-HerSau10-lambda-mu-Lambda-mu.pdf BibTex