[BGLS21] M. P. Bonacina, S. Graham-Lengrand, and N. Shankar. Conflict-driven satisfiability for theory combination: Lemmas, modules, and proofs. Journal of Automated Reasoning, 2021. [ bib | DOI | .pdf ]
(Subsumes Proofs in Conflict-Driven Theory Combination)
[AGLK20] B. Accattoli, S. Graham-Lengrand, and D. Kesner. Tight typings and split bounds, fully developed. Journal of Functional Programming, 30:e14, 2020. [ bib | DOI | https | .pdf ]
(Subsumes Tight Typings and Split Bounds and Tight Typings and Split Bounds - Long Version)
[BGLS19] M. P. Bonacina, S. Graham-Lengrand, and N. Shankar. Conflict-driven satisfiability for theory combination: Transition system and completeness. Journal of Automated Reasoning, 64(3):579--609, 2019. [ bib | DOI | .pdf ]
(Subsumes Satisfiability Modulo Theories and Assignments)
[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.99.