. Abst, inter s ( arrow s t)) t ( fun x : OK ( inter s ( arrow s t)) ? App s t (Proj_r s (arrow s t) x) ( Proj_l s ( arrow s t) x))

*. Judg, |-(lambda x:s. x) inter (lambda x:t. x) : (s ? s) inter

. Der, |-lambda x. x : (s union t) ? (t union s) *)

. Abst, union t s) ( fun x : OK ( union s t) ? Copair s t (union t s) ( Abst s ( union t s) ( fun y: OK s ? Inj_r t s y))

D. Aspinall and A. B. Compagnoni, Subtyping dependent types, Theor. Comput. Sci, vol.266, pp.1-2, 2001.

F. Barbanera, M. Dezani-ciancaglini, and U. Liguoro, Intersection and Union Types: Syntax and Semantics, Information and Computation, vol.119, issue.2, pp.202-230, 1995.
DOI : 10.1006/inco.1995.1086

F. Barbanera and S. Martini, Proof-functional connectives and realizability, Archive for Mathematical Logic, vol.1, issue.1, pp.189-211, 1994.
DOI : 10.1007/BF01203032

H. Barendregt, Introduction to generalized type systems, Journal of Functional Programming, vol.1, issue.2, pp.125-154, 1991.

H. Barendregt, The ?-Calculus with types, 2013.
DOI : 10.1017/CBO9781139032636

H. Barendregt, M. Coppo, and M. Dezani-ciancaglini, A filter lambda model and the completeness of type assignment, The Journal of Symbolic Logic, vol.37, issue.04, pp.931-940, 1983.
DOI : 10.1002/malq.19800261902

B. Barras and B. Bernardo, The Implicit Calculus of Constructions as a Programming Language with Dependent Types, FOSSACS, pp.365-379, 2008.
DOI : 10.1007/978-3-540-78499-9_26
URL : https://hal.archives-ouvertes.fr/inria-00432658

S. Berardi, Type dependence and Constructive Mathematics, Ph.D. Dissertation. University of Turin, 1990.

D. J. Dougherty, U. De-'liguoro, L. Liquori, and C. Stolze, A Realizability Interpretation for Intersection and Union Types, In APLAS (Lecture Notes in Computer Science), vol.12, issue.3, pp.187-205, 2016.
DOI : 10.1007/3-540-45927-8_9
URL : https://hal.archives-ouvertes.fr/hal-01317213

J. Daniel, L. Dougherty, and . Liquori, Logic and Computation in a Lambda Calculus with Intersection and Union Types, LPAR, pp.173-191, 2010.

J. Dunfield, Elaborating Intersection and Union Types, Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming, pp.17-28, 2012.
DOI : 10.1145/2398856.2364534
URL : http://arxiv.org/pdf/1206.5386

A. Richard, S. Eisenberg, and . Weirich, Dependently typed programming with singletons, Proc. ACM SIGPLAN Symposium on Haskell, pp.117-130, 2012.

A. Frisch, G. Castagna, and V. Benzaken, Semantic subtyping, Journal of the ACM, vol.55, issue.4, pp.1-1964, 2008.
DOI : 10.1145/1391289.1391293
URL : https://hal.archives-ouvertes.fr/hal-00152690

R. Harper, F. Honsell, and G. Plotkin, A framework for defining logics, Journal of the ACM, vol.40, issue.1, pp.143-184, 1993.
DOI : 10.1145/138027.138060

R. Harper and D. R. Licata, Mechanizing metatheory in a logical framework, Journal of Functional Programming, vol.40, issue.4-5, pp.4-5, 2007.
DOI : 10.1006/inco.2001.2951

J. and R. Hindley, Coppo-Dezani types do not correspond to propositional logic, Theoretical Computer Science, vol.28, issue.1-2, pp.235-236, 1984.
DOI : 10.1016/0304-3975(83)90074-9

P. Thomas and . Jensen, Disjunctive Strictness Analysis, Proc of LICS, pp.174-185, 1992.

L. Liquori and S. Rocca, Intersection Typed System à la Church, Information and Computation, vol.9, issue.205, pp.1371-1386, 2007.
URL : https://hal.archives-ouvertes.fr/hal-01149611

L. Liquori and C. Stolze, A Decidable Subtyping Logic for Intersection and Union Types, In TTCS (Lecture Notes in Computer Science, vol.19, issue.3, 2017.
DOI : 10.1016/S0019-9958(86)80019-5
URL : https://hal.archives-ouvertes.fr/hal-01560681

G. K. Edgar and . Lopez-escobar, Proof functional connectives, Methods in Mathematical Logic, pp.208-221, 1985.

D. B. Macqueen, G. D. Plotkin, and R. Sethi, An ideal model for recursive polymorphic types, Information and Control, vol.71, issue.1-2, pp.95-130, 1986.
DOI : 10.1016/S0019-9958(86)80019-5

K. Robert, R. Meyer, and . Routley, Algebraic analysis of entailment I, Logique et Analyse, vol.15, pp.407-428, 1972.

G. Mints, The completeness of provable realizability., Notre Dame Journal of Formal Logic, vol.30, issue.3, pp.420-441, 1989.
DOI : 10.1305/ndjfl/1093635158

A. Miquel, The Implicit Calculus of Constructions Extending Pure Type Systems with an Intersection Type Binder and Subtyping, In TLCA. (Lecture Notes in Computer Science), vol.2044, pp.344-359, 2001.
DOI : 10.1007/3-540-45413-6_27

A. Nuyts, A. Vezzosi, and D. Devriese, Parametric quantifiers for dependent type theory, Proceedings of the ACM on Programming Languages, vol.1, issue.ICFP, 2017.
DOI : 10.1145/99370.99404

N. Mishra-linger and T. Sheard, Erasure and Polymorphism in Pure Type Systems, FOSSACS, pp.350-364, 2008.
DOI : 10.1007/978-3-540-78499-9_25

F. Pfenning, Refinement types for logical frameworks, TYPES, pp.285-299, 1993.

C. Benjamin and . Pierce, Programming with intersection types, union types, and bounded polymorphism, 1991.

G. Pottinger, A Type Assignment for the Strongly Normalizable ?terms, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp.561-577, 1980.

C. John and . Reynolds, Preliminary Design of the Programming Language Forsythe, Report CMU?, pp.88-159, 1988.

V. Siles and H. Herbelin, Equality Is Typable in Semi-full Pure Type Systems, 2010 25th Annual IEEE Symposium on Logic in Computer Science, pp.21-30, 2010.
DOI : 10.1109/LICS.2010.19
URL : https://hal.archives-ouvertes.fr/inria-00496988

J. B. Wells and C. Haack, Branching Types, In ESOP (Lecture Notes in Computer Science), vol.2305, pp.115-132, 2002.
DOI : 10.1007/3-540-45927-8_9