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