[BGL13] A. Bernadet and S. Graham-Lengrand. Non-idempotent intersection types and strong normalisation. Logical Methods in Computer Science, 9(4), 2013. [ bib | DOI | http ] [pdf] (Subsumes Complexity of strongly normalising $\lambda$-terms via non-idempotent intersection types and Filter models: non-idempotent intersection types, orthogonality and polymorphism) [LDM11] S. Lengrand, R. Dyckhoff, and J. McKinna. A focused sequent calculus framework for proof search in Pure Type Systems. Logical Methods in Computer Science, 7(1), 2011. [ bib ] [pdf] (Subsumes A sequent calculus for Type Theory) [GL09] M. Gabbay and S. Lengrand. The λ-context calculus. Information and Computation, 207(12):1369--1400, 2009. [ bib ] (Subsumes The lambda-context calculus) [LM08] S. Lengrand and A. Miquel. Classical Fω, orthogonality and symmetric candidates. Annals of Pure and Applied Logic, 153:3--20, 2008. [ bib ] [pdf] (Subsumes A classical version of Fomega) [DL07] R. Dyckhoff and S. Lengrand. Call-by-value λ-calculus and LJQ. Journal of Logic and Computation, 17:1109--1134, 2007. [ bib | DOI ] [pdf] The proof of strong normalisation of LJQ: [pdf] (updated in December 2007) [KL07] D. Kesner and S. Lengrand. Resource operators for the λ-calculus. Information and Computation, 205:419--473, 2007. [ bib ] [pdf] (Subsumes Extending the Explicit Substitution Paradigm) [LLD+04] S. Lengrand, P. Lescanne, D. Dougherty, M. Dezani-Ciancaglini, and S. van Bakel. Intersection types for explicit substitutions. Information and Computation, 189(1):17--42, 2004. [ bib ] [pdf] (Subsumes An improved system of intersection types for explicit substitutions)

This file was generated by bibtex2html 1.98.