[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.