%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Abbreviations %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Journals
@STRING{AAML = {Archive for Mathematical Logic}}
@STRING{ACTA = {Acta Informatica}}
@STRING{AHC = {Annals of the History of Computing}}
@STRING{AI = {Artificial Intelligence}}
@STRING{AJM = {American Journal of Mathematics}}
@STRING{AML = {Archiv f\"ur Mathematische Logik und Grundlagenforschung}}
@STRING{ANN = {Annals of Mathematics}}
@STRING{APAL = {Annals of Pure and Applied Logic}}
@STRING{AU = {Algebra Universalis}}
@STRING{BAMS = {Bulletin of the American Mathematical Society}}
@STRING{BEATCS = {Bulletin of the European Association for
Theoretical Computer Science}}
@STRING{BSL = {Bulletin of Symbolic Logic}}
@STRING{CM = {Compositio Mathematica}}
@STRING{CPS = {Proceedings of the Cambridge Mathematical Society}}
@STRING{DMJ = {Duke Mathematical Journal}}
@STRING{ENTCS = {Electronic Notes in Computer Science}}
@STRING{FI = {Fundamenta In\-for\-ma\-ti\-cae}}
@STRING{FM = {Fundamenta Mathematicae}}
@STRING{IM = {Indagationes Mathematicae}}
@STRING{IPL = {Information Processing Letters}}
@STRING{JAR = {Journal of Automated Reasoning}}
@STRING{JACM = {Journal of the Association for Computing Machinery}}
@STRING{JCSS = {Journal of Computer and System Sciences}}
@STRING{JCTA = {Journal of Combinatorial Theory, Series (A)}}
@STRING{JCTB = {Journal of Combinatorial Theory, Series (B)}}
@STRING{JFP = {Journal of Functional Programming}}
@STRING{IANDC = {Information and Computation}}
@STRING{JLC = {Journal of Logic and Computation}}
@STRING{JLP = {Journal of Logic Programming}}
@STRING{JSC = {Journal of Symbolic Computation}}
@STRING{JSL = {Journal of Symbolic Logic}}
@STRING{LASC = {Lisp and Symbolic Computation}}
@STRING{LMCS = {Logical Methods in Computer Science}}
@STRING{LMS = {Proceedings of the London Mathematical Society}}
@STRING{LMSLNS = "London Mathematical Society Lecture Note Series"}
@STRING{MSCS = {Mathematical Structures in Computer Science}}
@STRING{MA = {Mathematische Annalen}}
@STRING{MJ = {Mathematica Japonica}}
@STRING{MZ = {Mathematische Zeitschrift}}
@STRING{NDJFL = {Notre Dame Journal of Formal Logic}}
@STRING{NG = {New Generation Computing}}
@STRING{PAMS = {Proceedings of the American Mathematical Society}}
@STRING{RAIRO = {RAIRO - Theoretical Informatics and Applications}}
@STRING{SCP = {Science of Computer Programming}}
@STRING{SIAM = {SIAM Journal of Computing}}
@STRING{SL = {Studia Logica}}
@STRING{SMD = {Soviet Mathematics Doklady}}
@STRING{TAMS = {Transactions of the American Mathematical Society}}
@STRING{TCS = {Theoretical Computer Science}}
@STRING{TOPLAS = {ACM Transactions on Programming Languages and Systems}}
@STRING{ZML = {Zeitschrift f\"ur Mathematischen Logik und Grundlagen der Mathematik}}
% Conferences
@STRING{ALP = {Algebraic and Logic Programming}}
@STRING{CAAP = {Colloquium on Trees in Algebra and Programming}}
@STRING{CSL = {Computer Science Logic}}
@STRING{CTRS = {International Workshop on Conditional and Typed Term Rewriteng Systems}}
@STRING{CW = {ACM SIGPLAN Workshop on Continuations}}
@STRING{ESOP = {European Symposium on Programming}}
@STRING{ICALP = {International Colloquium on Automata, Languages, and Programming}}
@STRING{ICFP = {International Conference on Functional Programming}}
@STRING{JICSLP = {Joint International Conference and Symposium on Logic programming}}
@STRING{LFCS = {Symposium on Logical Foundations of Computer Science}}
@STRING{LFP = {ACM Conference on Lisp and Functional Programming}}
@STRING{LPAR = {International Conference on Logic and Automated Reasoning}}
@STRING{FPCA = {Conference on Functional Programming and Computer Architecture}}
@STRING{GWFP = {Glasgow Workshop on Functional Programming}}
@STRING{HOA = {Higher Order Algebra, Logic and Term Rewriting}}
@STRING{ICLP = {International Conference on Logic Programming}}
@STRING{LICS = {Logic in Computer Science}}
@STRING{LOPSTR = {Logic Program Synthesis and Transformation}}
@STRING{MFCS = {Symposium on Mathematical Foundations of Computer Science}}
@STRING{MFPS = {Mathematical Foundations of Programming Semantics}}
@STRING{MFPLS = {Mathematical Foundations of Programming Language Semantics}}
@STRING{PEPM = {Proceeding of the ACM SIGPLAN Syposium on Partial Evaluation and Semantics-Based Program Manipulation}}
@STRING{PLILP = {Programming Languages: Implementations, Logics and Programs}}
@STRING{PLDI = {Programming Languages: Design and Implementation}}
@STRING{POPL = {Symposium on Principles of Programming Languages}}
@STRING{RTA = {Rewriting Techniques and Applications}}
@STRING{SAS = {Static Analysis Symposium}}
@STRING{STACS = {Symposium on Theoretical Aspects of Computer Science}}
@STRING{TACS = {Theoretical Aspects of Computer Software}}
@STRING{TAPSOFT = {Theory and Practice of Software Development}}
@STRING{TLCA = {Typed Lambda Calculi and Applications}}
@STRING{TYPES = {Types for Proofs and Programs}}
@STRING{WSA = {Workshop on Static Analysis}}
% Series
@STRING{CSLI = {CLSI Lecture Notes}}
@STRING{GTM = {Graduate Texts in Mathematics}}
@STRING{LNAI = {Lecture Notes in Artificial Intelligence}}
@STRING{LNCS = {Lecture Notes in Computer Science}}
@STRING{LNM = {Lecture Notes in Mathematics}}
@STRING{SLFM = {Studies in Logic and the Foundations of Mathematics}}
@STRING{CTTCS = {Cambridge Tracts in Theoretical Computer Science}}
% Institutions
@STRING{CCN = {Computing Center, No\-vo\-si\-birsk, USSR}}
@STRING{CMU = {Carnegie-Mellon University}}
@STRING{CWI = {Centre for Mathematics and Computer Science (CWI), Amsterdam}}
@STRING{CSI = {Computing Science Institute, University of Nijmegen}}
@STRING{DIKU = {Department of Computer Science, University of Copenhagen}}
@STRING{KUN = {University of Nijmegen}}
@STRING{KUL = {University of Leuven}}
@STRING{TUE = {Eindhoven University of Technology}}
@STRING{UU = {Utrecht University}}
@STRING{VUA = {Vrije Universiteit Amsterdam}}
% Publishers
@STRING{CUP = {Cambridge University Press}}
@STRING{IEEE = {IEEE Computer Society Press}}
@STRING{MH = {McGraw-Hill}}
@STRING{MIT = {MIT, Cambridge, Massachusetts}}
@STRING{NH = {North-Holland}}
@STRING{NYUP = {New York University Press}}
@STRING{PH = {Prentice-Hall}}
@STRING{OUP = {Oxford University Press}}
@STRING{PUP = {Princeton University Press}}
@STRING{SV = {Springer-Verlag}}
@STRING{AW = {Addison-Wesley}}
@STRING{CSLIP = {Center for the Study of Language and Information, Stanford}}
%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Bibliography %%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Bibliography %%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%% A %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@InProceedings{abrusci95lmslns,
Author = {Abrusci, V. Michele},
Title = {Noncommutative proof nets},
BookTitle = "Proceedings of the Workshop on Advances in Linear Logic,
Ithaca, New York June 1993",
institution= "Cornell Univesity",
editor = "Girard, Jean-Yves and Lafont, Yves and Regnier, Laurent",
Number = 222,
Series = LMSLNS,
Pages = {271--296},
Address = {Cambridge},
Publisher = cup,
year = 1995
}
@article{alesbarbdeza06,
number = {2},
volume = {355},
author = {Alessi, Fabio and Barbanera, Franco and Dezani-Ciancaglini,
Mariangiola},
title = {Intersection Types and Lambda Models},
journal = TCS,
year = 2006,
pages = {108--126}
}
@InProceedings{aleslusi02,
author = {Alessi, Fabio and Lusin, Stefania},
title = {Simple Easy Terms},
booktitle = {Intersection Types and Related Systems},
pages = {},
year = 2002,
volume = 70,
EDITOR = {van Bakel, S.},
series = ENTCS,
publisher = {Elsevier}
}
@article{alesdezalusi04,
number = {1--3},
volume = {316},
author = {Alessi, Fabio and Dezani-Ciancaglini, Mariangiola and Lusin,
Stefania},
journal = TCS,
title = {Intersection Types and Domain Operators},
year = {2004},
pages = {25--47},
}
@InProceedings{alti:lics01,
author = "Thorsten Altenkirch and Peter Dybjer and Martin Hofmann and Phil Scott",
title = "Normalization by evaluation for typed lambda calculus with coproducts",
pages = "303-310",
booktitle = LICS,
publisher = IEEE,
year = "2001"
}
@InProceedings{alti:flops04,
author = {Thorsten Altenkirch and Tarmo Uustalu},
title = {Normalization by evaluation for $\lambda^{\to 2}$},
booktitle = {Functional and Logic Programming},
isbn = {3-540-21402-X},
year = {2004},
volume = {2998},
series = LNCS,
pages = {260--275},
}
@article{anderson:1960,
AUTHOR="Anderson, A. R.",
TITLE="Entailment shorn of modality",
Journal=JSL,
Volume="25",
YEAR="1960",
Pages="388",
Note="(Abstract)"
}
@book{and/bel:1975,
author = "Anderson, A. R. and Belnap, N. D.",
title = "Entailment. The Logic of Relevance and Necessity, {V}olume~1",
Publisher = PUP,
Address = "U.S.A.",
year = 1975
}
@book{and/bel:1992,
author = "Anderson, A. R. and Bel{\-}nap, N. D. and Dunn, J. M.",
title = "Entailment. The Logic of Relevance and Necessity, {V}olume~2",
Publisher = PUP,
Address = "U.S.A.",
year = 1992
}
%%%%%%%%%%%%%% B %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@BOOK{barh84
, AUTHOR = {Barendregt, H.P.}
, TITLE = {The Lambda Calculus. {I}ts Syntax and Semantics}
, PUBLISHER = NH
, EDITION = {second}
, YEAR = 1984
}
@INPROCEEDINGS{barh-open,
AUTHOR = {Barendregt, H.P.},
TITLE = {Open problems},
PAGES = {367--370},
crossref = {|bohc75}
}
@article {barecoppdeza83,
AUTHOR = {Barendregt, Henk and Coppo, Mario and Dezani-Ciancaglini,
Mariangiola},
TITLE = {A filter lambda model and the completeness of type assignment},
JOURNAL = JSL,
VOLUME = {48},
YEAR = {1983},
NUMBER = {4},
PAGES = {931--940}
}
@InCollection{barendregt13turing,
author = {Henk Barendregt and Giulio Manzonetto},
title = {Turing's contributions to Lambda Calculus},
booktitle = {Alan Turing: His Work and Impact},
publisher = {Elsevier},
year = 2013,
editor = {S. Barry Cooper and Jan van Leeuwen},
pages = {139-143}}
@ARTICLE{Barthe:tcipts,
author = {Gilles Barthe},
title = {Type-checking injective Pure Type Systems},
journal = JFP,
year = {1998},
volume = {9},
pages = {675-698}
}
@INPROCEEDINGS{g95:tlca,
AUTHOR = {G. Barthe},
TITLE = {{Extensions of Pure Type Systems}},
PAGES = {16--31},
PSURL = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/tlca95.ps.gz},
crossref = {|dezm95}
}
@INPROCEEDINGS{g98:mfcs,
AUTHOR = {G. Barthe},
TITLE = {{The semi-full closure of Pure Type Systems}},
BOOKTITLE = {Proceedings of MFCS'98},
YEAR = 1998,
PUBLISHER = SV,
SERIES = LNCS,
VOLUME = {1450},
EDITOR = {L. Brim and J. Gruska and J. Zlatuska},
PAGES = {316--325},
PSURL = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/mfcs98.ps.gz}
}
@article{mhs:sorm2001,
author = "Gilles Barthe and John Hatcliff and Morten Heine S{\o}rensen",
title = "Weak normalization implies strong normalization in a class of non-dependent pure type systems",
journal = "Theoretical Computer Science",
volume = "269",
number = "1--2",
pages = "317--361",
year = "2001"}
@incollection {bera96,
AUTHOR = {Berarducci, Alessandro},
TITLE = {Infinite $\lambda$-calculus and non-sensible models},
BOOKTITLE = {Logic and Algebra (Pontignano, 1994)},
EDITOR = {A. Ursini and P. Aglian\`o},
PAGES = {339--377},
PUBLISHER = {Dekker},
YEAR = {1996},
}
@article{bergklop80,
author = {Jan A. Bergstra and
Jan Willem Klop},
title = {Invertible Terms in the Lambda Calculus},
journal = TCS,
volume = {11},
year = {1980},
pages = {19--37},
}
@article{berline00,
AUTHOR="Berline, Ch.",
TITLE="The lambda-calculus and its webbed models",
Journal=TCS,
Volume="249",
YEAR="2000",
Number="1",
Pages="81--161"
}
@article{berline06,
AUTHOR="Berline, Ch.",
TITLE="Graph models of lambda-calculus at work, and variations",
Journal=MSCS,
Volume="16",
YEAR="2006",
Pages="185--221"
}
@article{bimbo:2005,
AUTHOR="Bimb{\'o}, K.",
TITLE="Types of {I}-free hereditary
right maximal terms",
Journal="Journal of {P}hilosophical {L}ogic",
Volume="34",
YEAR="2005",
Pages="607--620"
}
@INCOLLECTION{bimbo:2006,
author = "Bimb{\'o}, K.",
title = "Relevance logics",
BOOKTITLE="{P}hilosophy of {L}ogic",
EDITOR="Jacquette, D.",
PUBLISHER="{N}orth-{H}olland/ {E}lsevier",
ADDRESS="Amsterdam",
SERIES= "Handbook of the {P}hilosophy of
{S}cience",
volume= 5,
year= 2006,
pages= "723--789"
}
@article{bimbo2013jsl,
volume = {78},
number = {1},
author = {Bimb\'o, Katalin and Dunn, J. Michael},
title = {On the Decidability of Implicational Ticket Entailment},
journal = JSL,
year = {2013},
pages = {214--236}
}
@Article{bros97,
author = {Broda, S. and Damas, L.},
title = {On combinatory complete sets of proper combinators},
journal = JFP,
year = {1997},
volume = {7},
number = {6},
pages = { 593--612}
}
@Article{bros04,
author = {Broda, S. and Damas, L. and M. Finger and P. Silva e Silva},
title = {The Decidability of a Fragment of {BB'IW}-Logic},
journal = TCS,
year = {2004},
volume = {318},
number = {3},
pages = {373--408}
}
%%%%%%%%%%%%%% C %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@article{carraro2012,
author = "Carraro, Alberto and Salibra, Antonino",
journal = RAIRO,
pages = "291--314",
title = "Easy lambda-terms are not always simple",
volume = 46,
year = 2012}
@BOOK{cur/fey:1958,
AUTHOR="H. B. Curry and R. Feys",
TITLE="Combinatory {L}ogic, {V}olume {I}",
PUBLISHER=NH,
ADDRESS={Amsterdam},
YEAR={1958},
NOTE="(3rd edition\ 1974)"
}
@BOOK{cur/hin/sel:1972,
AUTHOR="Curry, H. B. and Hindley, J. R. and Seldin, J. P. ",
TITLE="Combinatory {L}ogic, {V}olume~{II}",
PUBLISHER=NH,
ADDRESS={Amsterdam},
YEAR={1972}
}
%%%%%%%%%%%%%% D %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@Article{davr08,
author = {David, R.},
title = {A direct proof of the confluence of combinatory strong reduction},
journal = TCS,
year = 2009,
volume = 410,
number = 42,
pages = {4204-4215},
}
@article{dezahonlmoto05,
number = {3},
volume = {340},
author = {Dezani-Ciancaglini, Mariangiola and Honsell, Furio and Motohama,
Yoko},
title = {Compositional Characterization of $\lambda$-terms using Intersection
Types},
journal = TCS,
year = {2005},
pages = {459--495}
}
@Book{dicosmo,
author = {Di Cosmo, R.},
title = {Isomorphisms of Types: From $\lambda$-Calculus to
Information Retrieval and Language Design},
YEAR = 1995,
PUBLISHER = {Birkh\"auser}
}
@article{DHP95,
volume = {2},
number = 2,
tag = {Nordic Journal of Computing},
title = {Uncountable Limits and the Lambda Calculus},
author = {Di Gianantonio, Pietro and Honsell, Furio and Plotkin, Gordon},
pages = {126--145},
year = 1995,
journal = {Nordic Journal of Computing}
}
@inproceedings{deligu92,
author = {Ugo de'Liguoro and
Adolfo Piperno and
Richard Statman},
title = {Retracts in simply typed lambda-beta-eta-calculus},
booktitle = LICS,
year = {1992},
pages = {461--469},
publisher = IEEE
}
@article{Dougherty-Subrahmanyam,
author = {D. Dougherty and R. Subrahmanyam},
title = {Equality between functionals in the presence of coproducts},
journal = IANDC,
volume = 157,
pages = {52--83},
year = {2000}}
%%%%%%%%%%%%%% E %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%% F %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%% G %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@phdthesis{geuvers93logics,
author = "Herman Geuvers",
title = "Logics and Type Systems",
school ="Nijmegen University",
year = 1993,
url = "citeseer.ist.psu.edu/geuvers93logics.html" }
@InProceedings{ghani-tlca95,
author = {Ghani,N},
title = {Beta-Eta Equality for Coproducts},
pages = {171--185},
crossref = {|dezm95}
}
@article{Giannini-Ronchi:IeC-94,
volume = {110},
title = {A Type Inference Algorithm for a complete stratification of the
Polymorphic Type Discipline},
author = {Giannini, Paola and Ronchi Della Rocca, Simona},
pages = {115 - 173},
year = {1994},
journal = IANDC,
}
@Article{girj86,
author = {Girard, J.-Y.},
title = {The System {F} of variable Types, Fifteen years later},
journal = TCS,
year = 1986,
volume = 45,
pages = {159--192},
ignore = {Reprinted in~\cite{|hueg90}, pages~87--126}
}
@Article{girard91mscs,
Author = {Girard, Jean-Yves},
Title = {A New Constructive Logic: Classical Logic},
Journal = MSCS,
Volume = 1,
Number = 3,
Pages = {255--296},
fjournal = {Mathematical Structures in Computer Science. A Journal
in the Applications of Categorical, Algebraic and
Geometric Methods in Computer Science},
year = 1991
}
@article{940873,
author = {Inge Li G{\o}rtz and Signe Reuss and Morten Heine S{\o}rensen},
title = {Strong Normalization from Weak Normalization by Translation into the Lambda-{I}-Calculus},
journal = {Higher Order Symbol. Comput.},
volume = {16},
number = {3},
year = {2003},
issn = {1388-3690},
pages = {253--285},
publisher = {Kluwer Academic Publishers},
address = {Hingham, MA, USA},
}
@ARTICLE{GR:cecscpts,
author = {Guti{\'e}rrez, Francisco and Ruiz, Blas},
title = {Cut elimination in a class of sequent calculi for pure type systems},
journal = ENTCS,
year = {2003},
volume = {84},
pages = {105--116},
publisher = {Elsevier}
}
%%%%%%%%%%%%%% H %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@InProceedings{henre96,
author = "Henglein, F. and Rehof, J.",
title = "The Complexity of Subtype Entailment for Simple
Types",
booktitle = LICS,
year = "1997",
pages = "352--361",
publisher = IEEE
}
@InProceedings{henre98,
author = "Henglein, F. and Rehof, J.",
title = "Constraint Automata and the Complexity of
Recursive Subtype Entailment",
booktitle = ICALP,
year = "1998",
pages = {616--627},
publisher = SV,
series = LNCS,
volume ={1443}
}
@BOOK{hin/sel:1986,
Author="J. R. Hindley and J. P. Seldin",
Title="Introduction to {C}ombinators and {$\lambda$}-calculus",
Publisher=CUP,
Year=1986
}
@article {honsronc92,
AUTHOR = {Honsell, Furio and Ronchi Della Roc\-ca, Simona},
TITLE = {An approximation theorem for topological lambda models and the
topological incompleteness of lambda calculus},
JOURNAL = JCSS,
VOLUME = {45},
YEAR = {1992},
NUMBER = {1},
PAGES = {49--75}
}
@inProceedings{howard70slafm,
title = "Assignment of Ordinals to Terms for Primitive Recursive Functionals of Finite Type",
editor = "A. Kino, J. Myhill and R.E. Vesley",
booktitle = "Intuitionism and Proof Theory: Proceedings of the Summer Conference at Buffalo N.Y. 1968",
publisher = "Elsevier",
year = "1970",
volume = "60",
pages = "443 - 458",
series = SLFM,
author = "W.A. Howard",
}
@article {hyla76,
AUTHOR = {Hyland, Martin},
TITLE = {A syntactic characterization of the equality in some models
for the lambda calculus},
JOURNAL = {J. London Math. Soc. (2)},
VOLUME = {12},
YEAR = {1976},
NUMBER = {3},
PAGES = {361--370},
}
%%%%%%%%%%%%%% I %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@article{IntrigilaBiasone,
author = {Benedetto Intrigila and
E. Biasone},
title = {On the number of fixed points of a combinator in lambda
calculus},
journal = MSCS,
volume = {10},
number = {5},
year = {2000},
pages = {595-615},
}
@article{intrigila2010,
author = {Intrigila, Benedetto and Statman, Richard},
title = {Solution to the Range Problem for Combinatory Logic},
journal = FI,
volume = {111},
number = {2},
year = {2011},
pages = {203-222},
ee = {http://dx.doi.org/10.3233/FI-2011-560},
}
%%%%%%%%%%%%%% J %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@inproceedings{jaco75,
AUTHOR = {Jacopini, Giuseppe},
TITLE = {A Condition for Identifying Two Elements of Whatever Model
of Combinatory Logic},
PAGES = {213--219},
crossref = {|bohc75}
}
%%%%%%%%%%%%%% K %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@InProceedings{severidevries:CSL05,
author = {Severi, P. and {de} Vries, F. J.},
title = {Order structures for {B}{\"o}hm-like models},
booktitle = CSL,
volume = {3634},
pages = {103--116},
year = {2005},
series = LNCS,
publisher = SV
}
@InProceedings{kssv05,
author = {J.R. Kennaway and P. Severi and Sleep, M.R.
and {de} Vries, F. J.},
title = {Infinite rewriting: from syntax to semantics},
volume = {3838},
pages = {148--172},
booktitle = {Processes, Terms and Cycles: Steps on the Road to Infinity:
Essays Dedicated to Jan Willem Klop on the Occasion of His 60th Birthday},
year = {2005},
series = LNCS,
publisher = SV,
}
@Article{vrijer87IM,
author = {de Vrijer, R.},
title = {Exactly estimating functionals and strong normalization},
journal = IM,
year = 1987,
volume = 49,
pages = {479--493}}
@article{DBLP:journals/entcs/KetemaKO05,
author = {Jeroen Ketema and
Jan Willem Klop and
Vincent van Oostrom},
title = {Vicious Circles in Orthogonal Term Rewriting Systems.},
journal = ENTCS,
volume = {124},
number = {2},
year = {2005},
pages = {65-77}
}
@inproceedings{kurataka95,
aUthor = {Toshihiko Kurata and Masako Takahashi},
title = {Decidable Properties of Intersection Type Systems},
pages = {297--311},
crossref = {|dezm95}
}
@article{kura02,
author = {Toshihiko Kurata},
title = {Intersection and Singleton Type Assignment Characterizing
Finite {B}\"ohm-trees},
journal = IANDC,
volume = {178},
number = {1},
year = {2002},
pages = {1--11},
}
@inproceedings{kusd06,
AUTHOR = {Ku\'smierek, D.},
TITLE = {The inhabitation problem for rank two intersection types},
booktitle = TLCA,
year = 2007,
editor = {Ronchi Della Rocca, S.},
series={Lecture Notes in Computer Science},
volume={4583},
pages={240-254},
publisher = SV,
}
%%%%%%%%%%%%%% L %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@inproceedings{leid83,
AUTHOR = "Leivant, D.",
BOOKTITLE = POPL,
publisher = {ACM Press},
PAGES = "88--98",
TITLE = "Polymorphic Type Inference",
YEAR = "1983"}
%%%%%%%%%%%%%% M %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@inproceedings{DBLP:conf/csl/Malecki96,
author = {Sophie Malecki},
title = {Proofs in System ${F}_\omega$ Can Be Done in System
${F}_{\omega}^{\mbox{1}}$.},
editor = {van Dalen,~Dirk and
Marc Bezem},
booktitle = CSL,
publisher = SV,
series = LNCS,
volume = {1258},
year = {1997},
isbn = {3-540-63172-0},
pages = {297--315}
}
@Article{mccw91,
author = {William McCune and Larry Wos},
title = {The absence and the presence of fixed point combinators},
journal = TCS,
year = {1991},
volume = {87},
pages = {221--228}
}
@inproceedings{menn87,
AUTHOR = "Mendler, N.P.",
BOOKTITLE = LICS,
PAGES = "30--36",
PUBLISHER = IEEE,
TITLE = "Recursive Types and Type Constraints in
Second-Order Lambda Calculus",
YEAR = "1987"
}
@article{menn91
, AUTHOR = {Mendler, N.P.}
, JOURNAL = APAL
, PAGES = {159--172}
, TITLE = {Inductive Types and Type Constraints in the Second-Order
Lambda Calculus}
, VOLUME = {51}
, NUMBER = {1-2}
, YEAR = 1991
}
@Article{minp08,
author = {Minari, P.},
title = {A solution to {C}urry and {H}indley's problem on combinatory strong reduction},
journal = AAML,
year = 2009,
volume = {43}, number ={2},
pages = {159--184},
Publisher = SV,
obsoletenote = { Available at
\HREF{http://www.springerlink.com/content/6t75574g42413686}{SpringerLink}. },
}
%%%%%%%%%%%%%% N %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@article{NiehrenPriesnitz03,
author = "J. Niehren and T. Priesnitz",
journal = IANDC,
number = "2",
pages = "319--354",
title = "Non-structural subtype entailment in automata theory",
volume = 186,
year = 2003}
%%%%%%%%%%%%%% O %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%% P %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@InProceedings{padl01,
author= {Padovani, V.},
title = {Retracts in simple types},
BOOKTITLE = TLCA,
SERIES = LNCS,
PUBLISHER = SV,
volume ={2044},
YEAR = 2001,
editor ={Abramsky, S.},
pages ={376--384}
}
@Unpublished{padv10,
author = {Padovani, V.},
title = {Ticket {E}ntailment is decidable},
note = {Draft - Available \HREF{http://www.pps.jussieu.fr/\string ~padovani/te_mscs_draft.pdf}{HERE.}},
year = {2010}}
@article{padovani2013mscs,
author = {Padovani, Vincent},
title = {Ticket Entailment is decidable},
journal = MSCS,
volume = {23},
number = {3},
month = {6},
year = {2013},
issn = {1469-8072},
pages = {568--607},
numpages = {40},
doi = {10.1017/S0960129512000412},
annote = {{http://dx.doi.org/10.1017/S0960129512000412}},
eprint = {http://journals.cambridge.org/article_S0960129512000412},
}
@ARTICLE{Poll:epnpts,
author = {Poll, Erik},
title = {Theoretical Pearl: Expansion postponement for normalising Pure Type Systems},
journal = JFP,
year = {1998},
volume = {8},
pages = {89--96},
publisher = {Cambridge Univ Press}
}
@INPROCEEDINGS{Pollack:tpts,
author = {Randy Pollack},
title = {Typechecking in {Pure Type Systems}},
booktitle = {Informal Proceedings of the 1992 Workshop on Types for Proofs and
Programs, Bastad, Sweden},
year = {1992},
pages = {271--288}
}
@Unpublished{polonsky2010,
author = {Polonsky, A.},
title = {Failure of the range property for $\mathcal{H}$},
note = {Draft - Available \HREF{http://folk.uib.no/apo081/rp.ps}{HERE.}},
year = {2010}}
@article{polonsky2012jlc,
author = {Andrew Polonsky},
title = {The range property fails for {H}},
journal = JLC,
volume = {77},
number = {4},
year = {2012},
pages = {1195-1210},
}
@InProceedings{pottier96,
author = "Pottier, F.",
title = "Simplifying Subtyping Constraints",
booktitle = ICFP,
year = "1996",
pages = "122--133",
publisher = "ACM Press"
}
@book{polya2004book,
title={How to Solve It: A New Aspect of Mathematical Method},
author={P\'olya, G},
series={Penguin mathematics},
year={2004},
publisher={Princeton University Press},
note={Expanded
version of the 1988 edition, with a new foreword by John H. Conway},
}
%%%%%%%%%%%%%% Q %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%% R %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@phdthesis{ rehof98complexity,
author = "Jakob Rehof",
title = "The Complexity of Simple Subtyping Systems",
year = "1998",
school = DIKU,
}
@TechReport{regl01,
author = {L. Regnier and P. Urzyczyn},
title ={Retractions of types with many atoms},
institution = {IML Marseille},
year = 2001,
number ={29},
note ={{\tt http://arxiv.org/abs/cs/0212005}}
}
%%%%%%%%%%%%%% S %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@inproceedings{Simpson:TLCA:95,
author = {Simpson, A.K.},
title = {Categorical completeness results for simply-typed $\lambda$-calculus},
pages = {414--427},
crossref = {|dezm95}
}
@BOOK{smur85
, AUTHOR = {Smullyan, R.}
, TITLE = {To Mock a Mockingbird}
, PUBLISHER = {Knopf}
, YEAR = 1985
}
@PhdThesis{mhs:sorm97,
author = {S{\o}rensen, M.H.},
title = {Normalization in $\lambda$-Calculus and Type Theory},
school = DIKU,
note = {Available as DIKU Rapport 97/27},
year = 1997
}
@InProceedings{splz99,
author = {Sp{\l}awski, Z. and P. Urzyczyn},
title = {Type fixpoints: {I}teration vs.~recursion},
booktitle = ICFP,
year = 1999,
ignore = {editor = {P. Lee}},
publisher = {ACM Press},
pages = {102--113}
}
@article{Statman:AMLG:1983,
author = {Statman, R.},
title = {$\lambda $-definable functionals and $\beta \eta $ conversion},
journal = AML,
volume ={23},
year = {1983},
pages = {21--26}}
@TechReport{star7,
author = {Statman, R.},
title = {Three notes on combinatory algebra},
institution = {Department of Mathematics,
Carnegie Mellon University},
year = 1985,
number = {85-6}
}
@InProceedings{star86,
author = {Statman, R.},
title = {On translating lambda terms into combinators},
booktitle = LICS,
year = 1986,
publisher = IEEE,
pages = {378--382}
}
@TechReport{star8,
author = {Statman, R.},
title = {Combinators hereditarily of order one},
institution = {Department of Mathematics,
Carnegie Mellon University},
year = 1988,
number = {88-32}
}
@TechReport{star9,
author = {Statman, R.},
title = {Combinators hereditarily of order two},
institution = {Department of Mathematics,
Carnegie Mellon University},
year = 1988,
number = {88-33}
}
@ARTICLE{star89,
author = {Richard Statman},
title = {The Word Problem for {S}mullyan's {L}ark
Combinator is Decidable.},
journal = JSC,
volume = {7},
number = {2},
year = {1989},
pages = {103--112},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@TechReport{statman89cmu,
author = {Statman, Richard},
title = {Normal Varieties of Combinators},
institution = {Carnegie Mellon University, Department of Mathematical Sciences},
year = 1989,
number = 367,
note = {\newline The report can be found at \HREF{http://repository.cmu.edu/math/367/}{http://repository.cmu.edu/math/367/}}
}
@ARTICLE{star93,
author = {Statman, R.},
title = {Some examples of non-existent combinators},
journal = TCS,
year = 1993,
volume = 121,
pages = {441--448}
}
@inproceedings{star97,
author = {Richard Statman},
title = {Effective reduction and conversion strategies for
combinators},
booktitle = RTA,
year = {1997},
publisher = SV,
series = LNCS,
volume = {1232},
pages = {299--307}
}
@inproceedings{star00,
author = {Richard Statman},
title = {On the Word Problem for Combinators.},
booktitle = RTA,
year = {2000},
publisher = SV,
series = LNCS,
volume = {1833},
pages = {203--213},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@unpublished{statman2010,
author = {Richard Statman},
title = {To Type A Mockingbird},
year = {2010},
note ={A draft paper is available \HREF{http://tlca.di.unito.it/PAPER/TypeMock.pdf}{here}}
}
@article{stirling2009lmcs,
author = {Colin Stirling},
title = {Decidability of higher-order matching},
journal = LMCS,
volume = {5},
number = {3},
year = {2009},
ee = {http://arxiv.org/abs/0907.3804},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@InProceedings{SANPT02,
author = "Z. Su and A. Aiken and J. Niehren and
T. Priesnitz and R. Treinen",
Title = "The first-order theory of subtyping constraints",
booktitle = POPL,
year = "2002",
pages = "203--216",
publisher = {ACM Press}
}
%%%%%%%%%%%%%% T %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@inproceedings{tatsm07,
AUTHOR={Tatsuta, M.},
TITLE ={Types for Hereditary Permutators},
year = {2008},
booktitle = {Proceedings of the Twenty-Third Annual IEEE Symposium on
Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh,
PA, USA},
note ={\HREF{http://nii.ac.jp/TechReports/07-010E.html}
{http://nii.ac.jp/TechReports/07-010E.html}}
}
@ARTICLE{tri/hin/bun:1994,
AUTHOR="Trigg, P. and Hindley, J. R. and
Bunder, M. W.",
TITLE="Combinatory abstraction using {B}, {B'}
and friends",
JOURNAL=TCS,
VOLUME="135",
YEAR="1994",
PAGES="405--422"
}
@InProceedings{trismi96,
author = "Trifonov, V. and Smith, S.",
title = "Subtyping Constrained Types",
booktitle = SAS,
year = "1996",
pages = "349-365",
publisher = SV,
series = LNCS,
volume ={1145}
}
%%%%%%%%%%%%%% U %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@ARTICLE{urzp95
, AUTHOR = {Urzyczyn, P.}
, TITLE = {Positive Recursive Type Assignment}
, YEAR = 1996,
journal = FI,
volume = {28},
pages = {197--209},
number = {1-2}
}
@Article{urzp97a,
author = {Urzyczyn, P.},
title = {Type reconstruction in ${F}_\omega$},
journal = MSCS,
year = 1997,
volume = 7,
number = 4,
pages = {329--358},
}
@Article{urzy99,
author = {Urzyczyn, P.},
title = {The emptiness problem for intersection types},
journal = JSL,
year = {1999},
OPTkey = {},
volume = {64},
number = {3},
pages = {1195--1215},
OPTmonth = {},
note = {(Preliminary version in {\it Proc. LICS 94})},
OPTannote = {}
}
@InProceedings{urzp09,
author = {Urzyczyn, P.},
title = {Inhabitation of low-rank intersection types},
booktitle = TLCA,
year = 2009,
publisher = SV,
series = LNCS,
volume ={5608},
editor ={P.-L. Curien},
pages ={356--370}
}
%%%%%%%%%%%%%% V %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%% W %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@article {wads76,
AUTHOR = {Wadsworth, Christopher P.},
TITLE = {The relation between computational and denotational properties
for {S}cott's {$D\sb{\infty }$}-models of the lambda-calculus},
JOURNAL = SIAM,
VOLUME = {5},
YEAR = {1976},
NUMBER = {3},
PAGES = {488--521},
}
\bibitem{wilkweie12}
G.\ Wilken and A.\ Weiermann.
\newblock Derivation lengths classification of {G}{\"o}del's ${T}$ extending
{H}oward's assignment.
\newblock {\em Logical Methods in Computer Science}, 8(1):44, 2012.
@Article{wilken12lmcs,
author = {Gunnar Wilken and Andreas Weiermann },
title = {Derivation lengths classification of {G}{\"o}del's ${T}$ extending
{H}oward's assignment},
journal = LMCS,
year = 2012,
volume = 8,
number = 1,
pages = 44}
%%%%%%%%%%%%%% X %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%% Y %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%% Z %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%Cross-references %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@Book{|hueg90,
editor = {Huet, G.},
title = {Logical Foundations of Functional Programming},
booktitle = {Logical Foundations of Functional Programming},
publisher = AW,
year = 1990
}
@Book{|bohc75,
editor = {Corrado B{\"o}hm},
title = {$\lambda$-Calculus and Computer Science Theory},
booktitle = {$\lambda$-Calculus and Computer Science Theory},
YEAR = 1975,
PUBLISHER = SV,
SERIES = LNCS,
VOLUME = {37}
}
@PROCEEDINGS{|dezm95
, EDITOR = {Dezani-Ciancaglini, M. and Plotkin, G.}
, TITLE = TLCA
, BOOKTITLE = TLCA
, SERIES = LNCS
, VOLUME = {902}
, PUBLISHER = SV
, YEAR = 1995
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%