@article {mart83, AUTHOR = {Martin-L\"of}, TITLE = {domain interpretation of intuitionistic type theory}, } @article {long83, AUTHOR = {Longo, Giuseppe}, TITLE = {Set-theoretical models of $\lambda $-calculus: theories, expansions, isomorphisms}, JOURNAL = {Ann. Pure Appl. Logic}, FJOURNAL = {Annals of Pure and Applied Logic}, VOLUME = {24}, YEAR = {1983}, NUMBER = {2}, PAGES = {153--188}, ISSN = {0168-0072}, CODEN = {APALD7}, } @incollection {scot82, AUTHOR = {Scott, Dana S.}, TITLE = {Domains for denotational semantics}, BOOKTITLE = {Automata, languages and programming (Aarhus, 1982)}, PAGES = {577--613}, PUBLISHER = {Springer}, ADDRESS = {Berlin}, YEAR = {1982}, } @book {ales93, AUTHOR = {Alessi, Fabio}, TITLE = {modello p}, } @book {seve96, AUTHOR = {Severi, Paula}, TITLE = {PhD}, } @article {ronc88, AUTHOR = {Ronchi Della Rocca}, TITLE = {Dispense}, } @article {jaco75, AUTHOR = {Jacopini}, TITLE = {Easy}, } @article {baetboor, AUTHOR = {BB}, TITLE = {DeltaDelta}, } @article {dezamarg86, AUTHOR = {Dezani-Ciancaglini, Mariangiola and Margaria, Ines}, TITLE = {A characterization of ${F}$-complete type assignments}, JOURNAL = {Theoret. Comput. Sci.}, FJOURNAL = {Theoretical Computer Science}, VOLUME = {45}, YEAR = {1986}, NUMBER = {2}, PAGES = {121--157}, ISSN = {0304-3975}, CODEN = {TCSDI}, } %%%%AAAA @book{abragabbmaib92, editor="Abramsky, S. and Gabbay, Dov M. and Maibaum, T.S.E.", title={Handbook of Logic in Computer Science, Volume 2: Background: Computational Structures}, year={1992}, publisher={Oxford Science Publications}, tue={wis cbk 92 han} } @inproceedings{acze78, author={Aczel, P.}, title={The type theoretic interpretation of constructive set theory}, booktitle={Logic Colloquium '77}, note={Studies in Logic and the Foundations of Mathematics {\bf 96}}, editor="Macintyre, A. and Pacholski, L. and Paris, J.", publisher={North-Holland}, address={Amsterdam}, year={1978}, tue={wis cbl 71 log} } @inproceedings{acze80, author={Aczel, P.}, title={Frege structures and the notion of proposition, truth and set}, booktitle={The Kleene Symposium}, note={Studies in Logic and the Foundations of Mathematics {\bf 101}}, editor="Barwise, J. and Keisler, H. and Kunen, K.", publisher={North-Holland}, address={Amsterdam}, year={1980}, tue={wis cbn 80 kle} } @article{ajdu35, author={Ajdukiewicz, K.}, title={Die syntaktische {K}onnexit\"at}, journal={Studia Philosophica}, volume={1}, pages={1--27}, year={1935}, note={in German; English translation in \cite{mcca67}}, tue={Zie mcca67} } @mastersthesis{aleb94, author={Alebeek, E. van}, title={Isomorfie van beslisbare en opsombare ondergroepen van $(\q,+)$}, school={Department of Mathematics, Catholic University Nijmegen}, year={1994}, note={Dutch}, tue={IN BEZIT} } @incollection {alesbarb91, AUTHOR = {Alessi, Fabio and Barbanera, Franco}, TITLE = {Strong conjunction and intersection types}, BOOKTITLE = {Mathematical foundations of computer science, 1991 (Kazimierz Dolny, 1991)}, PAGES = {64--73}, PUBLISHER = {Springer}, ADDRESS = {Berlin}, YEAR = {1991}, } @PhdThesis{ales91, author = "Alessi, F.", title = "Strutture di tipi, teoria dei domini e modelli del lambda calcolo", school = "Torino University", year = "1991", OPTcrossref = "", OPTkey = "", address = "", OPTmonth = "", OPTtype = "", OPTnote = "", OPTannote = "" } BBBB @techreport{baetmauw94, author="Baeten, J.C.M. and Mauw, S.", title={Delayed Choice: An Operator for Joining Message Sequence Charts} , year={1994}, number={35}, institution={TUE Computing Science Reports}, address={Eindhoven University of Technology}, tue={IN BEZIT} } @article{barb95, author={Barbanera, F. and M. Dezani--Ciancaglini and U. de' Liguoro}, title={Intersection and union types: syntax and semantics}, journal={Information and Computation}, volume={119}, pages={202--230}, year={1995}, } @incollection{bare92, author={Barendregt, H.P.}, year={1992}, title={Lambda Calculi with types}, booktitle={{\rm\cite{abragabbmaib92}}}, publisher={Oxford University Press}, pages={117--309}, tue={wis CBK 92 HAN} } @incollection{bare96, author={Barendregt, H.P.}, year={1996}, title={The quest for correctness}, booktitle={Images of SMC Research}, publisher={Stichting Mathematisch Centrum}, address={P.O. Box 94079, 1090 GB Amsterdam}, pages={39--58} } @article{dekkbundbare97, author="Dekkers, W. and Bunder, M. and Barendregt, H.P.", title={Completeness of the propositions-as-types interpretation of intuitionistic logic into illative combinatory logic}, year={1997}, journal={The Journal of Symbolic Logic}, volume={To appear}, number={}, pages={}, tue={IN BEZIT} } @book{barwmoss96, author="Barwise, J. and Moss, L.", title="Vicious Circles", year={1996}, address={Stanford}, publisher={CSLI Publications}, tue={wis ...} } @book{benaputn83, editor="Benacerraf, P. and Putnam, H.", title={Philosophy of Mathematics}, publisher={Cambridge University Press}, year={1983}, edition={second}, tue={wis cbd 83 phi} } @article{bent78, author="Benthem, J.F.A.K. van", title="Four Paradoxes", year={1978}, journal="Journal of Philosophical Logic", volume="7", pages="49--72", tue={IN BEZIT} } @book{bent91, author={Benthem, J.F.A.K. van}, title={Language in Action: Categories, Lambdas and Dynamic Logic}, publisher={North-Holland}, year={1991}, series={Studies in Logic and the Foundations of Mathematics {\bf 130}}, address={Amsterdam}, tue={IN BEZIT} } @techreport{btjt81, author={Benthem Jutting, L.S. van}, title={Description of {A}{U}{T}-68}, year={1981}, number={12}, institution={Eindhoven University of Technology}, note={also in \cite{nedegeuvvrij94}}, tue={IN BEZIT} } @techreport{bera88, author={Berardi, S.}, title={Towards a mathematical analysis of the {C}oquand-{H}uet calculus of constructions and the other systems in {B}arendregt's cube}, year={1988}, institution={Dept. of Computer Science, Carnegie-Mellon University and Dipartimento Matematica, Universita di Torino}, tue={...} } @phdthesis{bera90, author={Berardi, S.}, title={Type Dependence and Constructive Mathematics}, year={1990}, school={Dipartimento Matematica}, address={Universit\`a di Torino}, tue={...} } @techreport{berabezecoqu94, author="Berardi, S. and Bezem, M.A. and Coquand, T.", title={On the computational content of the Axiom of Choice}, year={1994}, number={116}, institution={Department of Philosophy, Utrecht University}, tue={IN BEZIT} } @book{bergklopmidd89, author="Bergstra, J.A. and Klop, J.W. and Middeldorp, A.", title={Termherschrijfsystemen}, publisher={Kluwer Programmatuurkunde}, year={1989}, note={Dutch}, tue={wis dbn 89 ber} } @book{beth59, author={Beth, E.W.}, title={The Foundations of Mathematics}, publisher={North-Holland}, year={1959}, series={Studies in Logic and the Foundations of Mathematics}, address={Amsterdam}, tue={wis cbb 59 bet} } @mastersthesis{blee95, author={Bleeker, A.}, title={An Approach to Image Retrieval}, year={1995}, school={Katholieke Universiteit Nijmegen/Universit\`a di Padova}, tue={IN BEZIT} } @mastersthesis{bloo93, author={Bloo, R.}, title={Over de begrippen gefundeerd en verstrooid}, year={1993}, school={Department of Mathematics, Catholic University Nijmegen}, note={Dutch}, tue={IN BEZIT} } @techreport{bloo95, author={Bloo, R.}, title={Preservation of Strong Normalisation for Explicit Substitution}, institution={TUE Computing Science Notes}, address={Eindhoven University of Technology}, number={8}, year={1995}, month={mar}, tue={IN BEZIT} } @techreport{blookamanede94, author="Bloo, R. and Kamareddine, F. and Nederpelt, R.", title={Beyond $\beta$-Reduction in {C}hurch's $\lambda{\rightarrow}$}, institution={TUE Computing Science Notes}, address={Eindhoven University of Technology}, number={20}, year={1994}, month={apr}, tue={IN BEZIT} } @techreport{blookamanede94a, author="Bloo, R. and Kamareddine, F. and Nederpelt, R.", title={The $\lambda$-cube with classes of terms modulo conversion}, institution={TUE Computing Science Reports}, address={Eindhoven University of Technology}, number={46}, year={1994}, tue={IN BEZIT} } @techreport{blookamanede94b, author={Bloo, R. and Kamareddine, F. and Nederpelt, R.}, title={On {$\Pi$}-conversion in Type Theory}, institution={TUE Computing Science Reports}, address={Eindhoven University of Technology}, number={47}, year={1994}, tue={IN BEZIT} } @techreport{blookamanede94c, author={Bloo, R. and Kamareddine, F. and Nederpelt, R.}, title={The {B}arendregt {C}ube with {D}efinitions and {G}eneralised {R} eduction}, institution={TUE Computing Science Reports}, address={Eindhoven University of Technology}, number={34}, year={1994}, note={Also as Technical Report 8, University of Glasgow, Computing Science Department, 1994. To be published in Information and Computation}, tue={IN BEZIT} } @article{blookamanede95, author={Kamareddine, F. and Bloo, R. and Nederpelt, R.}, title={Definitions and {$\Pi$}-conversion in Type Theory}, year={1995}, journal={Submitted}, tue={Copie IN BEZIT} } @article{blookamanede96, author={Bloo, R. and Kamareddine, F. and Nederpelt, R.}, title={The {B}arendregt {C}ube with {D}efinitions and {G}eneralised {R}eduction}, year={1996}, journal={{I}nformation and {C}omputation}, volume={126}, number={2}, pages={123--143}, tue={IN BEZIT} } @phdthesis{borg94, author={Borghuis, V.A.J.}, title={Coming to Terms with Modal Logic: On the interpretation of modal ities in typed $\lambda$-calculus}, school={Technische Universiteit Eindhoven}, year={1994}, tue={IN BEZIT} } @phdthesis{boum93, author={Bouma, G.}, title={Nonmonotonicity and Categorial Unification Grammar}, school={Rijksuniversiteit Groningen}, year={1993}, tue={hfst. 1-3 in reader categoriale grammatica IN BEZIT} } @mastersthesis{bran95, author={Brands, J.}, title={Spelen met 0-1 wetten}, school={Department of Mathematics, Catholic University Nijmegen}, year={1995}, note={Dutch}, tue={IN BEZIT} } @mastersthesis{bron94, author={Bron, I.G.L.}, title={Benaderen van looptijden voor uittredingen die zich met zeer kle ine kans voordoen}, school={Department of Mathematics, Catholic University Nijmegen}, year={1994}, note={Dutch}, tue={IN BEZIT} } @phdthesis{brou07, author={{B}rouwer, L.E.J.}, title={Over de Grondslagen der Wiskunde}, school={Universiteit van Amsterdam}, year={1907}, note={Dutch; English translation in \cite{heyt75}}, tue={collected works: wis cae 75 bro; van dalen (ed): wis cbb 81 bro} } @article{brou18, author={Brouwer, L.E.J.}, title={Begr\"undung der {M}engenlehre unabh\"angig vom logischen {S}atz vom ausgeschlossenen {D}ritten}, journal={KNAW Verhandelingen}, year={1918}, volume={12}, number={5}, note={German; also in \cite{heyt75}}, tue={collected works: wis cae 75 bro} } @techreport{brui68, author={de Bruijn, N. G.}, title="{A}{U}{T}{O}{M}{A}{T}{H}, a language for mathematics", year={1968}, institution={T.H.-Reports}, number={68-{W}{S}{K}-05}, address={Eindhoven University of Technology}, tue={wis ARC 01 EUT} } @inproceedings{brui70, author={N. G. de Bruijn}, title={The mathematical language {A}{U}{T}{O}{M}{A}{T}{H}, its usage and some of its extensions}, booktitle={Symposium on Automatic Demonstration}, organization={Springer Verlag}, publisher={Berlin, 1970}, address={{I}{R}{I}{A}, Versailles}, editor="Laudet, M. and Lacombe, D. and Schuetzenberger, M.", pages={29--61}, year={1970}, note={Lecture Notes in Mathematics {\bf 125}; also in \cite{nedegeuvvrij94}}, tue={IN BEZIT} } @article {debr72, AUTHOR = {de Bruijn, N. G.}, TITLE = {Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the {C}hurch-{R}osser theorem}, JOURNAL = {Nederl. Akad. Wetensch. Proc. Ser. A {\bf 75}=Indag. Math.}, VOLUME = {34}, YEAR = {1972}, PAGES = {381--392}, } @inproceedings{debr68, author={N. G. de Bruijn}, title={The Mathematical Language {AUTOMATH}, Its Usage, and Some of Its Extensions}, editor={M. Laudet}, pages={29--61}, booktitle={Proceedings of the Symposium on Automatic Demonstratio n}, year={1968}, publisher={Springer-Verlag LNM 125}, address={Versailles, France}, month={dec}, keywords={Automath} } @techreport{brunkatokoymmauw93, author="Brunekreef, J. and Katoen, J.-P. and Koymans, R. and Mauw, S.", title={Design and Analysis of Dynamic Leader Election Protocols in Broa dcast Networks}, year={1993}, number={37}, institution={TUE Computing Science Notes}, address={Eindhoven University of Technology}, tue={IN BEZIT} } @article{bura97, author={Burali-Forti, C.}, title={Una questione su i numeri transfiniti}, year={1897}, journal={Rendiconti del Corcolo Matematico di Palermo}, volume={11}, note={English translation in \cite{heij67}, pages 104--112} } @article{burg86, author={Burgess, J.P.}, title={The Truth is Never Simple}, journal={Journal of Symbolic Logic}, volume={51}, pages={663--681}, year={1986}, tue={IN BEZIT} } @book{buszmarcbent88, editor="Buszkowski, W. and Marciszewski, W. and Benthem, J. van", title={Categorial Grammar}, publisher={John Benjamins}, year={1988}, series={Linguistic \&\ Literary Studies in Eastern Europe {\bf 25}}, address={Amsterdam}, tue={IPO-bibliotheek XF 88} } %CCCC @article{capr98, author={Capretta, V. and S. Valentini}, title={A general method for proving the normalization theorem for first and second order typed $\l$-calculi}, note={To appear}, journal={Mathematical Structures in Computer Science}, year={1998}, } @book{carn29, author={Carnap, R.}, title={Abriss der Logistik}, year={1929}, publisher={Springer Verlag}, address={Wien} } @book{carn65, author={Carnap, R.}, title={Foundations of Logic and Mathematics}, series={International Encyclopedia of Unified Science}, year={1965}, publisher={University of Chicago Press}, tue={wis cbb 65 car} } @article{chieturn88, author="Chierchia, G. and Turner, R.", title="Semantics and property theory", journal="Linguistics and Philosophy", volume="11", pages="261--302", year={1988}, tue={---} } @article{chur32, author={Church, A.}, title={A set of postulates for the foundation of logic (1)}, journal={Annals of Mathematics}, year={1932}, volume={33}, pages={346--366}, tue={IN BEZIT} } @article{chur33, author={Church, A.}, title={A set of postulates for the foundation of logic (2)}, journal={Annals of Mathematics}, year={1933}, volume={34}, pages={839--864}, tue={IN BEZIT} } @book{chur41, AUTHOR = {Church, A.}, TITLE = {The {C}alculi of {L}ambda-{C}onversion}, NOTE = {Annals of Mathematics Studies, no. 6}, PUBLISHER = {Princeton University Press}, ADDRESS = {Princeton, N. J.}, YEAR = {1941}, PAGES = {ii+77}, MRCLASS = {02.0X}, MRNUMBER = {3,129b}, MRREVIEWER = {H. B. Curry}, } @book{chur56, author={Church, A.}, title={Introduction to Mathematical Logic}, publisher={Princeton University Press}, year={1956}, tue={wis cbk 56 chu} } @article{chur76, author={Church, A.}, title={Comparison of {R}ussell's Resolution of the Semantic Antinomies with that of {T}arski}, journal={The Journal of Symbolic Logic}, year={1976}, volume={41}, pages={747--760}, tue={IN BIBLIOTHEEK WSK} } @article{churross36, author="Church, A. and Rosser, J.B.", title={Some properties of conversion}, journal={Transactions of the American Mathematical Society}, year={1936}, volume={39}, pages={472--482}, tue={IN BEZIT} } @book{consETAL86, author={Constable et al., R.L.}, title="Implementing Mathematics with the Nuprl Proof Development System", year={1986}, publisher={Prentice-Hall}, address={New Jersey}, tue={DGR 6 IMP} } @phdthesis{coqu85, author={Coquand, T.}, title={Une th\'eorie des constructions}, year={1985}, school={Universit\'e Paris VII}, address={Th\`ese de troisi\`eme cycle}, tue={...} } @inproceedings{coqu86, author={Coquand, T.}, title={An Analysis of {G}irard's Paradox}, booktitle={Proceedings of the Symposium on Logic in Computing Science}, year={1986}, address={Cambridge, Massachusetts}, organization={IEEE}, tue={IN BEZIT} } @article{coquhuet88, author="Coquand, T. and Huet, G.", title="The Calculus of Constructions", journal="Information and Computation", year={1988}, volume={76}, pages={95--120}, tue={...} } @book{curi86, author = {Curien, P.-L.}, title = {Categorical Combinators, Sequential Algorithms, and Functional Programming}, series = {Research Notes in Theoretical Computer Science}, publisher = {Pitman}, address = {London}, year = {1986}, pages = {xviii+300}, isbn = {0-273-08722-3}, comments = {available in U.S. from John Wiley and Sons}, checked = {7 November 1990} } @article{couscurimaun87, author = {G.~Cousineau and P.-L.~Curien and M.~Mauny}, title = {The categorical abstract machine}, journal = {Science of Computer Programming}, volume = {8(2)}, pages = {173--202}, year = {1987} } @article{curi86a, title = {Categorical Combinators}, author = {P.-L. Curien}, pages = {188--254}, journal = {Information and Control}, month = {apr / may / jun}, year = {1986}, volume = {69}, number = {1--3} } @article{curr29, author={Curry, H.B.}, year={1929}, title={An Analysis of Logical Substitution}, journal={American Journal of Mathematics}, volume={51}, pages={363--384}, tue={IN BEZIT} } @article{curr30, author={Curry, H.B.}, year={1930}, title={Grundlagen der kombinatorischen {L}ogik}, journal={American Journal of Mathematics}, volume={52}, pages={509--536, 789--834}, note={German}, tue={IN BEZIT} } @article{curr34, author={Curry, H.B.}, year={1934}, title={Functionality in combinatory logic}, journal={Proceedings of the National Academy of Science of the USA}, volume={20}, pages={584--590}, tue={IN BEZIT} } @book{curr63, author={Curry, H.B.}, year={1963}, title={Foundations of Mathematical Logic}, publisher={McGraw-Hill Book Company, Inc.}, series={McGraw-Hill Series in Higher Mathematics}, tue={wis cbk 63 cur} } @book{currfeys58, author="Curry, H.B. and Feys, R.", year={1958}, title={Combinatory Logic}, publisher={North-Holland}, address={Amsterdam}, volume={I}, series={Studies in Logic and the Foundations of Mathematics}, tue={wis cbk 58 cur} } @book{currhindseld72, author="Curry, H.B. and Hindley, J.R. and Seldin, J.P.", year={1972}, title={Combinatory Logic}, publisher={North-Holland}, address={Amsterdam}, volume={II}, series={Studies in Logic and the Foundations of Mathematics}, tue={wis cbk 72 cur} } %DDDD @inproceedings{daal73, author="Daalen, D.T. van", title="A description of {A}utomath and some aspects of its language theory", editor="Braffort, P.", booktitle="Proceedings of the Symposium APLASM", year="1973", volume="I", note="Also in \cite{nedegeuvvrij94}", tue={IN BEZIT} } @phdthesis{daal80, author={Daalen, D.T. van}, title="The Language Theory of Automath", year="1980", school="Eindhoven University of Technology", tue="wis cbk 80 daa" } @book{dale78, author={Dalen, D. van}, title={Filosofische grondslagen van de wiskunde}, publisher={Van Gorcum}, year={1978}, address={Assen, Amsterdam}, note={Dutch}, tue={IN BEZIT} } @book{dale81, editor={Dalen, D. van}, title={Over de Grondslagen der Wiskunde}, publisher={Mathematisch Centrum}, year={1981}, address={Amsterdam}, note={Dutch; L.E.J. Brouwers' Thesis together with unpublished fragment s, correspondence with D.J. Korteweg, review by G. Mannoury, and an introduction}, tue={cbb 81 bro} } @article{dalefreukrol81, author="Dalen, D. van and Freudenthal, H. and Krol, G.", title={De wiskundige {B}rouwer en de eenzaamheid van het gelijk}, journal={Vrij Nederland}, year={1981}, month={feb}, note={Dutch}, tue={caz 81 dal} } @techreport{damsgrumgert94, author="Dams, D. and Grumberg, O. and Gerth, R.", title={Abstract Interpretation of Reactive Systems: Abstractions Preser ving $\al$CTL*, $\er$CTL* and CTL*}, year={1994}, number={24}, institution={TUE Computing Science Notes}, address={Eindhoven University of Technology}, tue={IN BEZIT} } @article{davi73, author={Davis, M.}, title={Hilbert's tenth problem is unsolvable}, journal={American Mathematical Monthly}, volume=80, year=1973, pages={233--269} } @book{dede72, author="Dedekind, R.", title={Stetigkeit und irrationale Zahlen}, address={Braunschweig}, year={1872}, publisher={\mbox{}}, tue={...} } @article {dekk88, AUTHOR = {Dekkers, Wil}, TITLE = {Reducibility of types in typed lambda calculus. {C}omment on: ``{O}n the existence of closed terms in the typed $\lambda$-calculus, {I}'' (\ncite{stat80})}, JOURNAL = {Inform. and Comput.}, FJOURNAL = {Information and Computation}, VOLUME = {77}, YEAR = {1988}, NUMBER = {2}, PAGES = {131--137}, ISSN = {0890-5401}, } @unpublished{dekk93, author={Dekkers, W.}, title={Lambda calculus en herschrijfsystemen}, note={Lecture notes W7-HL, Catholic University of Nijmegen}, year={1993}, tue={IN BEZIT} } @proceedings{dezaplot95, editor="Dezani-Ciancaglini, M. and Plotkin, G.", title={Second International Conference on Typed Lambda Calculi and Applications, TLCA'95}, year={1995}, series={Lecture Notes in Computer Science}, number={902}, publisher={Springer Verlag}, tue={IN BEZIT}, address={Berlin} } @techreport{dose90, author={Dosen, K.}, title={A Brief Survey of Frames for the {L}ambek Calculus}, institution={Konstanzer Berichte zur Logik und Wissenschaftstheorie}, year={1990}, number={5}, tue={IN BEZIT reader categoriale grammatica} } @techreport{dowe91, author={{Dowek et al.}, G.}, title={The {C}oq {P}roof {A}ssistant {V}ersion 5.6, {U}sers {G}uide}, year={1991}, institution={INRIA}, number={134}, address={Le Chesney} } @phdthesis{draa95, author={Draanen, J.-P. van}, year={1995}, title={Models for simply typed lambda-calculi with fixed point combinators and enumerators}, school={Catholic University of Nijmegen}, tue={IN BEZIT} } @article{dyck97, author={Dyckhoff, R. and L. Pinto}, title={Permutability of proofs in intuitionistic sequent calculi}, note={To appear}, journal={Theoretical Computer Science}, year={1997}, } @article{dyck98, author={Dyckhoff, R. and L. Pinto}, title={Permutability of proofs in intuitionistic sequent calculi}, note={To appear}, journal={Theoretical Computer Science}, year={1998}, } %EEEE @misc{elbe96, author={Elbers, H.}, title={Personal communication}, year=1996 } @misc{eucl00, author={Euclid}, title={{T}he {E}lements}, howpublished={325 B.C. English translation in \cite{heat56}} } %FFFF @inproceedings{fefe78, author={Feferman, S.}, booktitle={Logic Colloquium '78}, year={1978}, editor={Boffa, M. and Dalen, D. van and McAloon, K}, title={Constructive Theories of Functions and Classes}, publisher={North Holland}, address={Amsterdam}, pages={159--224}, tue={IN BEZIT} } @article{fefe84, author={Feferman, S.}, title={Toward useful type-free theories {I}}, journal={Journal of Symbolic Logic}, volume={49}, year={1984}, pages={75--111}, tue={IN BEZIT} } @book{frae27, author={Fraenkel, A.}, title={Zehn Vorlesungen \"uber die Grundlegung der Mengenlehre}, year={1927}, publisher={B.G. Teubner}, address={Leipzig, Berlin}, series={Wissenschaft und Hypothese, Band XXXI}, note={German}, tue={ruu wis fr 01 1} } @book{frae28, author={Fraenkel, A.}, title={Einleitung in die Mengenlehre}, year={1928}, publisher={Springer Verlag}, address={Berlin}, series={Die Grundlehren der mathematischen Wissenschaften in Einzeldars tellungen mit besonderer Ber\"ucksichtigung der Anwendungsgebiete, Band IX}, edition={third}, note={German}, tue={ruu wis fr 01 2a} } @book{fraebarhlevy73, author="Fraenkel, A.A. and Bar-Hillel, Y. and Levy, A.", title={Foundations of Set Theory}, publisher={North Nolland}, year={1973}, series={Studies in Logic and the Foundations of Mathematics 67}, address={Amsterdam}, edition={second}, tue={wks cbf 58 fra} } @book{freg79, author={Frege, G.}, title={Begriffschrift, eine der arithmetischen nachgebildete Formelspra che des reinen Denkens}, publisher={Nebert}, address={Halle}, year={1879}, note={Also in \cite{heij67}, pages 1--82}, tue={in wis cbl 67 fro} } @book{freg84, author={Frege, G.}, title={Grundlagen der Arithmetik}, address={Breslau}, publisher={\mbox{}}, year={1884}, note={(also in \cite{benaputn83})}, tue={in wis cbd 83 phi} } @book{freg92, author={Frege, G.}, title={Grundgesetze der Arithmetik, begriffsschriftlich abgeleitet}, address={Jena}, publisher={\mbox{}}, year={1892}, volume={I}, note={Reprinted 1962 (Olms, Hildesheim)}, tue={...} } @book{freg03, author={Frege, G.}, title={Grundgesetze der Arithmetik, begriffsschriftlich abgeleitet}, address={Jena}, publisher={Pohle}, year={1903}, volume={II}, note={Reprinted 1962 (Olms, Hildesheim)}, tue={...} } @incollection{frie75, author={Friedman, H.M.}, title={Equality between functionals}, booktitle={Logic {C}olloqium}, editor={Parikh, R.}, year={1975}, series={Lecture Notes in Mathematics}, volume={453}, publisher={Springer}, address={Berlin, New York}, pages={} } %GGGG @inproceedings{gand77, author={Gandy, R.O.}, title={The Simple Theory of Types}, booktitle={Logic Colloquium '76}, publisher={North-Holland}, editor="Gandy, R.O. and Hyland, J.M.E.", year={1977}, pages={173--181}, address={Amsterdam}, note={Studies in Logic and the Foundations of Mathematics {\bf 87}}, tue={wis cbl 71 log} } @incollection{gand80, author={Gandy, R.}, title={An early proof of normalization by {A}.~{M}.~{T}uring}, booktitle={To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism}, editor="J. P. Seldin and J. R. Hindley", publisher={Academic Press}, address={New York}, pages={453--457}, year={1980}, } author={Gentzen, G.}, title={Die Widerspruchsfreiheit der {S}tufenlogik}, journal={Mathematische Zeitschrift}, year={1930}, volume={41}, pages={357--366}, note={German}, tue={IN BEZIT} } @article{gent36, author={Gentzen, G.}, title={Untersuchungen \"uber das logischen {S}chliessen}, journal={Mathematische Zeitschrift}, volume={39}, year={1936}, pages={405--431}, note={Translation in: {\emph{Collected papers of Gerhard Gentzen}}, ed. M. E. Szabo, North-Holland, Amsterdam [1969], pp.\ 68--131} } @booklet{gerh90, author={{Gerhardt, editor}, C.I.}, title={Die Philosophischen {S}chriften von {G}ottfried {W}ilhelm {L}eib niz}, year={1890}, address={Berlin}, tue={...} } @techreport{gert94, author="Gerth, editor., R. ", title={Verifying Sequentially Consistent Memory}, institution={TUE Computing Science Reports}, year={1994}, address={Eindhoven University of Technology}, number={44}, tue={IN BEZIT} } @misc{geuv90, author="Geuvers, J.H.", title="Type Systems for Higher Order Predicate Logic", year={1990}, month={May}, howpublished={Manuscript, Catholic University of Nijmegen}, tue={???} } @phdthesis{geuv93, author={Geuvers, J.H.}, title={Logics and Type Systems}, school={Catholic University of Nijmegen}, year={1993}, tue={IN BEZIT} } @article{geuvnede91, author="Geuvers, J.H. and Nederhof, M.J.", title={A modular proof of strong normalization for the {C}alculus of {C}onstructions}, journal={Journal of Functional Programming}, year={1991}, volume={1}, number={2}, pages={155--189}, tue={...} } @book{gierhofm80, author={Gierz, Gerhard K. and Hofmann, Karl Heinrich and Keimel, Klaus and Lawson Jimmie D. and Mislove, Michael W. and Scott, Dana S.}, title={A Compendium of Continuous Lattices}, publisher={Springer-Verlag}, address={Berlin}, year={1980}, } @misc{gira72, key={Girard 72}, author={Girard, J.-Y.}, title={Interpretation fonctionelle et elimination des coupures de l'arithmetique d'ordre superieur}, howpublished={These D'Etat, Universite Paris VII}, year={1972} } @inproceedings{gira95, author={Girard, J.-Y.}, title={Linear logic: its syntax and semantics}, booktitle={Advances in linear logic}, editor={J.-Y. Girard and Y. Lafont and L. Regnier}, year={1995}, publisher={London Mathematical Society Lecture Note Series, Cambridge University Press}, note={Available by anonymous ftp from lmd.univ-mrs.fr as /pub/girard/Synsem.ps.Z} } @book{giralafotayl89, author={Jean-Yves Girard and Lafont, Yves G. A. and Paul Taylor}, title={Proofs and Types}, publisher={Cambridge University Press}, series={Cambridge Tracts in Theoretical Computer Science}, volume={7}, camlib={[Univ. Lib.] 348:8.b.95.26}, year={1989} } @article{goed31, author={G\"odel, K.}, title={{\"U}ber formal unentscheidbare {S}\"atze der {P}rincipia {M}athematica und verwandter {S}ysteme {I}}, journal={Monatshefte f\"ur {M}athematik und {P}hysik}, volume={38}, year={1931}, pages={173--198}, note={German; English translation in \cite{heij67}, pages 592--618}, TUE={in heij67} } @incollection{goed44, author={G\"odel, K.}, title={Russell's mathematical logic}, booktitle={The Philosophy of Bertrand Russell}, publisher={Evanston \&\ Chicago, Northwestern University}, year={1944}, editor={Schlipp, P.A.}, note={Also in \cite{benaputn83}}, tue={in wis cbd 83 phi} } @article{goed80, author={G\"odel, K.}, title={On a hitherto unexploited extension of the finitary standpoint}, journal={Journal of Philosophical Logic}, year={1980}, volume={9}, pages={133--142}, note={English translation of \cite{goed58}, with a bibliography added}, tue={IN BEZIT} } @book{gordmelh93, editor={Gordon, M.J.C. and Melham, T.F.}, title={Introduction to HOL: A Theorem Proving Environment for Higher Order Logic}, publisher={Cambridge University Press}, year={1993}, address={London/New York} } %HHHH @book {harretal85, TITLE = {Harvey {F}riedman's research on the foundations of mathematics}, EDITOR = {Harrington, L. A. and Morley, M. D. and {\v{S}}{\v{c}}edrov, A. and Simpson, S. G.}, SERIES = {Studies in Logic and the Foundations of Mathematics}, VOLUME = {117}, PUBLISHER = {North-Holland Publishing Co.}, ADDRESS = {Amsterdam}, YEAR = {1985}, PAGES = {xvi+408}, ISBN = {0-444-87834-3}, } @book{haeg94, author={Haegeman, L.}, title={Introduction to Government \& Binding Theory}, publisher={Blackwell}, address={Oxford}, year={1994}, edition={second}, tue={KUB LET E HAEG 1994} } @book{heat56, author={Heath, T.L.}, title={The Thirteen Books of Euclid's Elements}, publisher={Dover Publications, Inc.}, address={New York}, year={1956}, tue={wis CFD 56 EUC} } @book{heij67, editor={Heijenoort, J. van}, title={From Frege to G\"odel: A Source Book in Mathematical Logic, 1879 --1931}, publisher={Harvard University Press}, address={Cambridge, Massachusetts}, year={1967}, tue={wis cbl 67 fre} } @phdthesis{hend93, author={Hendriks, H.}, title={Studied Flexibility: Categories and Types in Syntax and Semantic s}, school={Universiteit van Amsterdam}, year={1993}, tue={IN BEZIT} } @article{henk50, author={Henkin, L.}, year={1950}, volume={15}, journal={The Journal of Symbolic Logic}, title={Completeness in the Theory of Types}, pages={81--91}, tue={IN BEZIT} } @article{henk63, author={Henkin, L.}, year={1963}, pages={323--344}, volume={52}, journal={Fundamentae Mathematicae}, title={A Theory of Propositional Types}, tue={IN BEZIT} } @inproceedings{herb95, author={Herbelin, H.}, title={A lambda calculus structure isomorphic to {G}entzen-style sequent calculus structure}, booktitle={Computer {S}cience {L}ogic ({C}{S}{L}'94)}, series={Lecture Notes in Computer Science {\bf 933}}, publisher={Springer Verlag}, address={Berlin}, pages={61--75}, year={1995}, } @mastersthesis{heum92, author={Heumen, R. van}, title={Een intu\"{\i}tionistische verkenning van de constructie van {V} itali}, school={Department of Mathematics, Catholic University Nijmegen}, year={1992}, note={Dutch}, tue={IN BEZIT} } @book{heyt34, author={Heyting, A.}, title="Mathematische Grundlagenforschung. Intuitionismus. Beweistheorie ", publisher={Springer Verlag}, address={Berlin}, series={Ergebnisse der Mathematik und ihrer Grenzgebiete}, year={1934}, tue={ipo cz 3} } @book{heyt56, author={Heyting, A.}, title={Intuitionism, an introduction}, year={1956}, address={Amsterdam}, series={Studies in Logic and the Foundations of Mathematics}, publisher={North Holland}, tue={...} } @book{heyt75, editor={Heyting, A.}, title={Brouwer: Collected Works}, publisher={North-Holland}, address={Amsterdam}, volume={1}, year={1975}, tue={wis cae 75 bro} } @article{hilb26, author={Hilbert, D.}, title={\"{U}ber das {U}nendliche}, journal={Mathematische Annalen}, volume={95}, year={1926}, note={Also in \cite{heij67}, pages 367--392}, tue={wis cbl 67 fro} } @book{hilbacke28, author="Hilbert, D. and Ackermann, W.", title={Grundz\"uge der Theoretischen Logik}, publisher={Springer Verlag}, address={Berlin}, year={1928}, series={Die Grundlehren der Mathematischen Wissenschaften in Einzeldars tellungen, Band XXVII}, edition={first}, tue={exemplaar Nederpelt; 4e editie: tue wis} } @article{hind69, author={Hindley, R.}, title={The Principal Type-Scheme of an Object in Combinatory Logic}, year={1969}, volume={146}, pages={29--60}, journal={Transactions of the American Mathematical Society}, tue={IN BEZIT} } @book{hind97, author={Hindley, J.R.}, title={Basic Simple Type Theory}, publisher={Cambridge University Press}, address={Cambridge, UK}, year={1997} } @inproceedings{howa80, author={Howard, W.A.}, title={The formulas-as-types notion of construction}, booktitle={To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism}, editor="Seldin, J.P. and Hindley, J.R.", year={1980}, publisher={Academic Press}, address={New York}, pages={479--490}, tue={...} } @unpublished{hube94, author={Hubey, H.M.}, title={On Hilbert's First Problem}, year={1994}, note={Montclair State College}, tue={IN BEZIT} } @phdthesis{hurk93, author={Hurkens, A.J.C.}, title={Borel determinacy without the axiom of choice}, school={Catholic University Nijmegen}, year={1993}, tue={IN BEZIT} } %IIII @book{iver62, author={Iverson, K.E.}, title={A programming language}, school={Catholic University Nijmegen}, year={1962}, publisher={Wiley}, address={New York}, tue={ } } %JJJJ @phdthesis{jack95, author={Jackson, P.B.}, title={Enhancing the Nuprl Proff Development System and Applying it to Computational Abstract Algebra}, year={1962} } @unpublished{jack95a, author={Jackson, P.B.}, title={The {N}uprl Proof Development System, {V}ersion 4.1 Reference Manual and User's Guide}, year={1995}, note={Cornell University, Department of Computing Science, Ithaca, New York.}, tue={IN BEZIT} } @unpublished{jaco94, author={Jacobs, B.}, title={Quotients in Simple Type Theory}, note={Draft version of 30 March 1994}, tue={IN BEZIT} } @mastersthesis{jurj92, author={Jurjus, H.H.}, title={Groepen van permutaties van de natuurlijke getallen, mede in ver band met de theorie van berekenbare functies}, year={1992}, school={Vakgroep Wiskunde, Katholieke Universiteit Nijmegen}, note={Dutch}, tue={IN BEZIT} } %KKKK @article{kama92a, author={Kamareddine, F.}, title={$\lambda$-Terms, Logic, Determiners and Quantifiers}, year={1992}, journal={Journal of Logic, Language and Information}, volume={1}, pages={79--103}, tue={IN BEZIT} } @article{kama92b, author={Kamareddine, F.}, title={Set Theory and Nominalisation}, year={1992}, journal={Journal of Logic and Computation}, volume={2}, pages={579--604, 687--707}, tue={IN BEZIT} } @article{kama92c, author={Kamareddine, F.}, title={A system at the cross-roads of functional and logic programming} , year={1992}, journal={Science of Computer Programming}, volume={19}, pages={239--279}, tue={IN BEZIT} } @techreport{kama92d, author={Kamareddine, F.}, title={Are Types needed for Natural Language?}, year={1992}, number={20}, institution={TUE Computing Science Notes}, address={Eindhoven University of Technology}, tue={IN BEZIT} } @article{kamaklei93, author="Kamareddine, F. and Klein, E.", title={Nominalization, Predication and Type Containment}, year={1993}, journal={Journal of Logic, Language and Information}, volume={2}, pages={171--215}, tue={IN BEZIT} } @techreport{kamalaan95a, author="Kamareddine, F. and Laan, T.", title="A Reflection on {R}ussell's Ramified Types and {K}ripke's Hierar chy of Truths", year={1995}, institution={TUE Computing Science Notes}, number={18}, address={Eindhoven University of Technology}, tue={IN BEZIT}, } @techreport{kamalaan95b, author="Kamareddine, F. and Laan, T.", title="{K}ripke's Theory of Truth and {A}czel's {F}rege Structures", year={1995}, institution={TUE Computing Science Notes}, tue={IN BEZIT}, note={In preparation} } @article{kamalaan96, author="Kamareddine, F. and Laan, T.", title="A Reflection on {R}ussell's Ramified Types and {K}ripke's Hierar chy of Truths", year={1996}, journal="Journal of the Interest Group in Pure and Applied Logic", volume={4}, number={2}, pages={195--213}, tue={IN BEZIT}, note={{\tt http://www.mpi-sb.mpg.de:80/igpl/Bulletin/V4-2/Kamareddine.d vi.gz}} } @techreport{kamalaan96a, author="Kamareddine, F. and Laan, T.", title="A {C}orrespondence between {N}uprl and the {R}amified {T}heory o f {T}ypes", year={1996}, institution="TUE Computing Science Notes", tue={EIGEN WERK}, number="12", note="Also as Technical Report~TR-1996-18, Department of Computing Science, University of Glasgow, 1996" } @article{kamanede93, author="Kamareddine, F. and Nederpelt, R.", title={On stepwise explicit substitution}, journal={International Journal of Foundations of Computer Science}, volume={4}, pages={197--240}, year={1993}, tue={IN BEZIT} } @techreport{kamanede94, author="Kamareddine, F. and Nederpelt, R.P.", title={Canonical typing and {$\Pi$}-conversion}, year={1994}, number={2}, institution={TUE Computing Science Notes}, address={Eindhoven University of Technology}, tue={IN BEZIT} } @article{kamanede96, author="Kamareddine, F. and Nederpelt, R.P.", title={Canonical typing and {$\Pi$}-conversion in the {B}arendregt {C}u be}, year={1996}, volume={6}, number={2}, pages={245--267}, journal={Journal of Functional Programming}, tue={IN BEZIT} } @article{kamanede94b, author="Kamareddine, F. and Nederpelt, R.P.", title={A unified approach to type theory through a refined $\lambda$-ca lculus}, year={1994}, volume={136}, journal={Theoretical Computer Science}, pages={183--216}, tue={IN BEZIT} } @techreport{kanz91, author={Kanzawa, M.}, year={1991}, title={The Lambek Calculus enriched with additional connectives}, institution={ITLI Prepublications for Logic, Semantics and Philosophy o f Language}, tue={IN BEZIT reader categoriale grammatica} } @article{klee34, author={Kleene, S.C.}, title={Proof by cases in formal logic}, year={1934}, journal={Annals of Mathematics}, volume={35}, pages={529--544}, tue={IN BEZIT} } @article{klee35, author={Kleene, S.C.}, title={A theory of positive integers in formal logic}, year={1935}, journal={American Journal of Mathematics}, volume={57}, pages={153--173, 219--244}, tue={IN BEZIT} } @article{klee36, author={Kleene, S.C.}, title={Lambda-definability and recursiveness}, journal={Duke Mathematical Journal}, year={1936}, volume={2}, pages={340--353}, tue={IN BEZIT} } @book{klee52, author={Kleene, S.C.}, title={Introduction to Metamathematics}, series={The University Series in Higher Mathematics}, year={1952}, publisher={D. Van Nostrand Comp.}, address={New York, Toronto}, tue={wis cbd 52 kle} } @article{kleeross35, author="Kleene, S.C. and Rosser, J.B.", title={The inconsistency of certain formal logics}, year={1935}, journal={Annals of Mathematics}, volume={36}, pages={630--636}, tue={IN BEZIT} } @PhdThesis{klop80, author = "Klop, J.W.", title = "Combinatory Reduction Systems", school = "Utrecht University", year = "1980", note = "Appeared as Mathematical Centre Tracts 127, Kruislaan 413, 1098 SJ Amsterdam", OPTannote = "" } @incollection{klop92, author={Klop, J.W.}, title={Term Rewriting Systems}, booktitle={{\rm \cite{abragabbmaib92}}}, year={1992}, pages={1--116}, publisher={Oxford University Press}, tue={wis cbk 92 han} } @book{kneaknea62, author="Kneale, W. and Kneale, M.", title={The Development of Logic}, year={1962}, publisher={Oxford University Press}, tue={wm bft 62 kne} } @book{knee63, author={Kneebone, G.T.}, year={1963}, title={Mathematical Logic and the Foundations of Mathematics}, publisher={D. Van Nostrand Comp.}, address={London, New York, Toronto}, tue={exemplaar Nederpelt} } @phdthesis{koge95, author="Kogel, E. de", year={1995}, title={Equational Proofs in Tableaux and Logic Programming}, school={Tilburg University}, address={Tilburg}, tue={IN BEZIT} } @article{kolm32, author={Kolmogorov, A.N.}, title={Zur {D}eutung der {I}ntuitionistischen {L}ogik}, journal={Mathematisches Zeitschrift}, pages={58--65}, volume={35}, year={1932}, tue={...} } @inproceedings{krei59, author={Kreisel, G.}, title={Interpretation of Analysis by means of Constructive Functionals of Finite Types}, booktitle={Constructivity in Mathematics}, year={1959}, editor={Heyting, A.}, pages={101--128}, publisher={North-Holland}, address={Amsterdam}, note={Studies in Logic and the Foundations of Mathematics}, tue={wis cbv 59 con} } @incollection{krei70, author={Kreisel, G.}, title={Church's Thesis: a kind of reducibility axiom for constructive mathematics}, crossref={myhi70}, booktitle={Intuitionism and proof theory}, pages={121--150} } @book{kriv90, AUTHOR = {Krivine, Jean-Louis}, TITLE = {Lambda-calcul Types et mod\`eles}, PUBLISHER = {Masson}, ADDRESS = {Paris}, YEAR = {1990}, PAGES = {viii+176}, ISBN = {2-225-82091-0}, NOTE = {English translation \ncite{kriv93}.} } @book{kriv93, AUTHOR = {Krivine, J.-L.}, TITLE = {Lambda-calculus, types and models}, NOTE = {Translated from the 1990 French original by Ren\'e Cori}, PUBLISHER = {Ellis Horwood}, ADDRESS = {New York}, YEAR = {1993}, PAGES = {viii+180}, ISBN = {0-13-062407-1}, } @proceedings{myhi70, editor={Myhill, J. and Vesley, R. E. and Kino, A.}, booktitle={Intuitionism and proof theory}, publisher={North-Holland}, address={Amsterdam}, organization={Studies in Logic and the Foundations of Mathematics}, year=1970 } @article{krei70a, author={Kreisel, G.}, title={The formalist-positivist doctrine of mathematical precision in the light of experience}, journal={L'age de la Science}, volume=3, year=1970, pages={17--46} } @article{krip75, author={Kripke, S.}, title={Outline of a Theory of Truth}, journal={Journal of Philosophy}, volume={72}, year={1975}, pages={690--716}, tue={---} } @phdthesis{kupe94, title={Partiality in Logic and Computation}, author={Kuper, J.}, year={1994}, school={University of Twente}, address={Enschede}, tue={IN BEZIT} } %LLLL @mastersthesis{laan93, author={Laan, T.}, title={Spelen met Oneindig in de intu\"{\i}tionistische wiskunde}, school={Department of Mathematics, Catholic University Nijmegen}, year={1993}, note={Dutch}, tue={IN BEZIT} } @techreport{laan94, author={Laan, T.}, year={1994}, number={33}, title={A Formalization of the {R}amified {T}ype {T}heory}, institution={TUE Computing Science Reports}, address={Eindhoven University of Technology}, tue={EIGEN WERK} } @inproceedings{laan95a, author={Laan, T.}, title={{A} {M}odern {V}iew on the {R}amified {T}heory of {T}ypes}, booktitle={{P}roceedings {C}{S}{N} 95}, editor={Vliet, J.C. van}, year={1995}, publisher={{S}tichting {M}athematisch {C}entrum}, address={Amsterdam}, pages={122--133}, tue={EIGEN WERK} } @techreport{laan96a, author={Laan, T.}, year={1996}, title={{\sc Automath} and {P}ure {T}ype {S}ystems}, institution={TUE Computing Science Reports}, address={Eindhoven University of Technology}, number="11", tue={EIGEN WERK} } @article{laannede96, author={Laan, T. and Nederpelt, R.P.}, year={1996}, title={{A} Modern Elaboration of the {R}amified {T}heory of {T}ypes}, journal={Studia Logica}, volume={57}, number={3}, tue={EIGEN WERK} } @article{lamb58, author={Lambek, J}, year={1958}, title={The mathematics of sentence structure}, journal={American Mathematical Monthly}, volume={65}, pages={154--170}, note={Also in \cite{buszmarcbent88}}, tue={in XF 88 (IPO), 153-172}, } @article{lambscot81, author="Lambek, J. and Scott, P.J.", year={1981}, title={Intuitionist type theory and foundations}, journal={Journal of Philosophical Logic}, volume={10}, pages={101--115}, tue={IN BEZIT} } @mastersthesis{leuw95, author={Leuw, B.-J. de}, title={Generalisations in the lambda calculus and its type theory}, year={1995}, school={Department of Computing Science, Catholic University of Nijmegen}, tue={IN BEZIT} } @book{lloy93, author={Lloyd, J.W.}, year={1993}, title={Foundations of Logic Programming}, edition={second}, publisher={Springer Verlag}, address={Berlin}, series={Symbolic Computation -- Artificial Intelligence}, tue={IN BEZIT} } @techreport{long86, author={Longo, G.}, title={On {C}hurch's Formal Theory of Functions and Functionals}, year={1987}, number={9}, institution={Department of Computing Science, Pisa University}, tue={Exemplaar Nederpelt} } @misc{luo, author={Luo, Z.}, title={{E}{C}{C} and extended {C}alculus of {C}onstructions}, howpublished={Department of Computer Science, University of Edinburgh}, tue={...} } @misc{luo_94, author={Luo, Z.}, title={On the totality of propositions in type theory}, year={1994}, howpublished={Submitted for TLCA '95}, tue={IN BEZIT} } %MMMM @article {mair92, AUTHOR = {Mairson, Harry G.}, TITLE = {A simple proof of a theorem of {S}tatman}, JOURNAL = {Theoret. Comput. Sci.}, FJOURNAL = {Theoretical Computer Science}, VOLUME = {103}, YEAR = {1992}, NUMBER = {2}, PAGES = {387--394}, ISSN = {0304-3975}, CODEN = {TCSDI}, } @incollection{mati71, author={Matijasevi{\v{c}}, Yu. V.}, title={On recursive unsolvability of Hilbert's tenth problem}, booktitle={Fourth International Congress for Logic, methodology and philosophy of science}, year={1971}, publisher={North-Holland}, address={Amsterdam}, pages={89--110}, note={Studies in Logic and the Foundations of Mathematics {\bf 74}}, } @Book{mcca62, author= "{John McCarthy {\it et al.}}", title= "LISP 1.5 Programmer's Manual", publisher= "MIT Press", year= 1962, address= "Cambridge, Massachusetts" } @inproceedings{mart75, author={Martin-L\"of, P.}, title={An intuitionistic theory of types: predicative part}, booktitle={Logic Colloquium '73}, editor="Rose, H.E. and Shepherdson, J.C.", year={1975}, publisher={North-Holland}, address={Amsterdam}, pages={73--118}, note={Studies in Logic and the Foundations of Mathematics {\bf 80}}, tue={wis cbl 71 log} } @inproceedings{mart82, author={Martin-L\"of, P.}, title={Constructive mathematics and computer programming}, booktitle={Sixth International Congress for Logic, Methodology and Philosophy of Science}, year={1982}, publisher={North-Holland}, address={Amsterdam}, pages={153--175}, tue={???} } @book{mart84, author={Martin-L\"of, P.}, title={Intuitionistic Type Theory}, series={Studies in Proof Theory}, year={1984}, publisher={Bibliopolis}, address={Napoli}, tue={wis cbk 84 mar} } @techreport{mauwmeul95, author="Mauw, S. and Meulen, E.A. van der", title="Specification of tools for {M}essage {S}equence {C}harts", year={1995}, number={17}, institution={TUE Computing Science Reports}, address={Eindhoven University of Technology}, tue={IN BEZIT} } @techreport{mauwreni94, author="Mauw, S. and Reniers, M.A.", title={An Algebraic Semantics of Basic Message Sequence Charts}, year={1994}, number={17}, institution={TUE Computing Science Notes}, address={Eindhoven University of Technology}, tue={IN BEZIT} } @techreport{mauwreni95, author="Mauw, S. and Reniers, M.A.", title={Empty Interworkings and Refinement Semantics of Interworkings Re vised}, year={1995}, number={12}, institution={TUE Computing Science Reports}, address={Eindhoven University of Technology}, tue={IN BEZIT} } @techreport{mauwmuld94, author="Mauw, S. and Mulder, H.", title={Regularity of {B}{P}{A}-Systems is Decidable}, year={1994}, number={27}, institution={TUE Computing Science Notes}, address={Eindhoven University of Technology}, tue={IN BEZIT} } @book{mcca67, editor={McCall, S.}, title={Polish Logic 1920--1939}, year={1967}, publisher={Oxford University Press}, address={London}, tue={Koninklijke Bibliotheek 7028 C 14} } @article{melh93, author={Melham, T.F.}, title={The {H}{O}{L} Logic Extended with Quantification over Type Varia bles}, year={1993}, pages={7--24}, journal={Formal Methods in System Designs}, tue={IN BEZIT} } @Book{milntoftharp90, author= "Robin Milner and Mads Tofte and Robert Harper", title= "The Definition of {S}tandard {ML}", publisher= "The MIT Press", year= 1990 } @incollection{mint96, author={Mints, G.}, title={Normal forms for sequent derivations}, booktitle={Kreiseliana. About and Around Georg Kreisel}, editor="P. Odifreddi", publisher={A.K. Peters, Wellesley}, address={Massachusetts}, pages={469--492}, year={1996}, } @Article{moggi91, author= "Eugenio Moggi", title= "Notions of Computation and Monads", journal= "Information and Computation", year= 1991, volume= 93, pages= "55-92" } @incollection{mont73, author={Montague, R.}, editor="Hintikka, J. and Moravcsik, J.M.E. and Suppes, P.", booktitle="Approaches to Natural Language", title="The proper treatment of quantification in ordinary {E}nglish", year={1973}, publisher={Dordrecht}, tue={---} } @phdthesis{moor88, author={Moortgat, M.}, year={1988}, school={University of Utrecht}, title={Categorial Investigations: Logical and Linbuistical Aspects of t he Lambek Calculus}, tue={cm apy 88 moo} } @misc{mooroehr93, author="Moortgat, M. and Oehrle, D.", title={Lecture Notes on Categorial Grammar}, howpublished={Fifth European Summer School in Language, Logic and Infor mation, Lisbon}, year={1993}, month={aug}, tue={IN BEZIT reader categoriale grammatica} } @misc{morr??, author={Morrill, G.}, title={Discontinuity and Pied-Piping in Categorial Grammar}, tue={IN BEZIT, reader categoriale grammatica} } @techreport{morr92, author={Morrill, G.}, title={Type-Logical Grammar}, year={1992}, number={2}, month={jan}, institution={OTS Working Papers}, tue={IN BEZIT} } %NNNN @book{nede87, author="Nederpelt, R.P.", title="De taal van de wiskunde", year="1987", publisher="Versluys", address="Almere", tue="wis cbk 87 ned" } @book{nedegeuvvrij94, editor="Nederpelt, R.P. and Geuvers, J.H. and Vrijer, R.C. de", title={Selected Papers on Automath}, publisher={North-Holland}, year={1994}, series={Studies in Logic and the Foundations of Mathematics {\bf 133}}, address={Amsterdam}, tue={IN BEZIT} } @article{nedekama92, author="Nederpelt, R.P. and Kamareddine, F.", title="A useful lambda notation", journal="The Journal of Symbolic Logic", year={1992}, note="Paper presented at the 1992 Logic Colloquium, Vesprem, Hungary", } @mastersthesis{nies93, author={Niesten, S.}, year={1993}, title={Minstens \&\ {H}oogstens}, school={Department of Mathematics, Catholic University Nijmegen}, note={Dutch}, tue={IN BEZIT} } @proceedings{nieu95, editor={Nieuwendijk, A.}, title={Accolade '94}, year={1995}, organization={Dutch Graduate School in Logic}, tue={IN BEZIT} } %OOOO @book{odon77, author={O'Donnell, M.J.}, title={Computing in Systems Described by Equations}, volume={58}, series={Lecture Notes in Computer Science}, publisher={Springer Verlag}, year={1977}, tue={---} } @mastersthesis{oost96, author={Oostdijk, M.}, year={1996}, title={\\{P}roof by Calculation}, school={385, Universitaire School voor Informatica, Catholic University Nijmegen}, volume={385}, tue={IN BEZIT} } %PPPP @Unpublished{park76, author = "Park, D.", title = "The ${\Y}$-combinator in {S}cott's $\l$-calculus models (revised version)", note = "Theory of Computation Report 13, Department of Computer Science, University of Warick", OPTcrossref = "", OPTkey = "", year = "1976", OPTannote = "" } @article{pars71, author={Parsons, C.}, title={The iterative conception of Set}, journal={The Journal of Philosophy}, volume={68}, year={1971}, pages={215--237}, tue={IN BEZIT} } @incollection{pars79, author={Parsons, T.}, year={1979}, title="The theory of types and ordinary language", booktitle="Linguistics, Philosophy and Montague Grammar", editor={Davies, S. and Mithun, M.}, publisher="University of Texas Press", address={Austin}, tue={---} } @book{pean89, author={Peano, G.}, year={1889}, title={Arithmetices principia, nova methodo exposita}, publisher={Bocca}, address={Turin}, note={English translation in \cite{heij67}, pages 83--97} } @techreport{pelehuizpete94, author="Peleska, J. and Huizing, C. and Petersohn, C.", title={A Comparison of {W}ard \&\ {M}ellor's Transformation Schema with State- \&\ Activitycharts}, year={1994}, number={11}, institution={TUE Computing Science Notes}, address={Eindhoven University of Technology}, tue={IN BEZIT} } @techreport{pent92, author={Pentus, M.}, title={Lambek grammars are context free}, year={1992}, institution={Department of Mathematical Logic, Faculty of Mechanics and Mathematics, Moscow University}, tue={IN BEZIT reader categoriale grammatica} } @techreport{pere94, author={Peremans, W.}, title={Ups and Downs of Type Theory}, institution={TUE Computing Science Notes}, year={1994}, number={14}, address={Eindhoven University of Technology}, tue={IN BEZIT} } @mastersthesis{pete92, author={Peters, R.H.M.T.}, title={Oorsprong van de Typentheorie}, year={1992}, school={Eindhoven University of Technology}, note={Dutch}, tue={IN BEZIT} } @Article{pott81, author = "Pottinger, G.", title = "The Church-Rosser theorem for the typed $\l$-calculus with surjective pairing", journal = "Notre Dame J. Formal Logic", year = "1981", volume = "22", number = "3", pages = "264--268" } @phdthesis{poll94, author={Poll, E.}, title={A Programming Logic Based on Type Theory}, school={Eindhoven University of Technology}, year={1994}, tue={IN BEZIT} } @article{pott77, author={Pottinger, G.}, title={Normalization as a homomorphic image of cut--elimination}, journal={Annals of Mathematical Logic}, volume={12}, pages={323--357}, year={1977}, } @Article{prav97, author = "Pravato, A. ", title = "Categorical Models of Untyped Lambda Calculi: a Monoidal Approach", OPTcrossref = "", OPTkey = "", journal = "", OPTyear = "1997", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", note = "PHD thesis", OPTannote = "" } @Article{pravroncrove99, author = "Pravato, A. and Ronchi, S. and Roversi, L.", title = "The call-by-value lambda calculus: a semantic investigation", journal = "Mathematical structures in computer science", OPTyear = "1999", OPTvolume = "9", OPTnumber = "5", OPTpages = "617--650", } @book{praw65, author={Prawitz, D.}, title="Natural Deduction", year="1965", publisher="Almqvist \&\ Wiksell", address="Stockholm", tue="wis cbk 65 pra" } @book{gierhoffkeimmislscot80, author={Gierz, G.K. and Hoffmann, K.H. and Keimel, K. and Mislove, J.D. and Scott, D.S.}, title="A Compendium of Continuous Lattices", year="1980", publisher="Springer-Verlag", address="Berlin", } @incollection{praw71, author={Prawitz, D.}, title={Ideas and results in proof theory}, booktitle={Proceedings of the 2nd Scandinavian Logic Symposium}, editor="J. E. Fenstad", publisher={North-Holland}, address={Amsterdam}, pages={235--307}, year={1971}, } %QQQQ @article{quin37, author={Quine, W.~Van Orman}, title={New Foundations for Mathematical Logic}, year={1937}, journal={American Mathematical Monthly}, volume={44}, note={Also in \cite{quin61a}}, tue={wm bft 61 van} } @book{quin52, author={Quine, W.~Van Orman}, title={Methods of Logic}, year={1952}, publisher={Routledge \&\ Kegan Paul}, address={London}, tue={wm bft 58 orm} } @article{quin61, author={Quine, W.~Van Orman}, title={Paradox}, journal={Scientific American}, volume={206}, year={1962}, note={Also in \cite{quin66}}, tue={quin66, wm bec 66 qui} } @book{quin61a, author={Quine, W.~Van Orman}, title={From a Logical Point of View: 9 Logico-Philosophical Essays}, publisher={Harvard University Press}, address={Cambridge, Massachusetts}, year={1961}, tue={wm bft 61 van} } @book{quin63, author={Quine, W.~Van Orman}, title={Set Theory and its Logic}, publisher={Harvard University Press}, address={Cambridge, Massachusetts}, year={1963}, tue={wm cbk 63 qui} } @book{quin66, author={Quine, W.~Van Orman}, title={The Ways of Paradox and other essays}, publisher={Random House}, address={New York}, year={1966}, tue={wm bec 66 qui} } %RRRR @techreport{raamseve95, author="Raamsdonk, F. van and Severi, P.", title="On Normalisation", year={1995}, number={20}, institution={Computing Science Notes}, address={Eindhoven University of Technology}, tue={IN BEZIT} } @article{rams25, author={Ramsey, F.P.}, year={1925}, title={The Foundations of Mathematics}, journal={Proceedings of the London Mathematical Society}, pages={338--384}, tue={IN BEZIT} } @unpublished{rave94, author={Raven, D.}, year={1994}, title={The Enculturation of Logical Practice}, note={Essay}, tue={IN BEZIT via logicagroep Sarlemijn/Kroes} } @InProceedings{reyn72, author= "John C. Reynolds", title= "Definitional Interpreters for Higher-Order Programming Languages", booktitle= "Proceedings of 25th {ACM} National Conference", year= 1972, pages= "717-740", OPTorganization= "ACM", address= "Boston, Massachusetts" } @InProceedings{reyn74, author= "John C. Reynolds", title= "On the Relation between Direct and Continuation Semantics", booktitle= "2nd Colloquium on Automata, Languages and Programming", year= 1974, editor= "Jacques Loeckx", series={Lecture Notes in Computer Science}, number=14, pages= "141-156", OPTpublisher=S-V, address= "Saarbr{\"{u}}cken, West Germany", month= Jul } @book{riemwill86, author="Riemsdijk, H. van and Williams, E.", year={1986}, title={Introduction to the Theory of Grammar}, publisher={Massachusetts Institute of Technology Press}, address={Cambridge, Massachusetts}, series={Current Studies in Linguistics {\bf 12}}, tue={KUB LET e4 RIEM 1986} } @phdthesis{rooi63, author={Rooij, A.C.M. van}, title={On lattices of rings of sets}, school={Utrecht University}, year={1963}, tue={IN BEZIT} } @phdthesis{roor91, author={Roorda, D.}, title={Resource Logics: Proof-theoretical investigations}, school={University of Amsterdam}, year={1991}, tue={IN BEZIT reader categoriale grammatica} } @proceedings{rootstaa68, editor="Rootselaar, B. van and Staal, J.F.", year={1968}, title={Logic, Methodology and Philosophy of Science III}, publisher={North-Holland, Amsterdam}, address={Amsterdam}, organization={Studies in Logic and the Foundations of Mathematics}, tue={wis cbd 62 log} } @article{ross35, author={Rosser, J.B.}, title={A mathematical logic without variables}, journal={Annals of Mathematics}, volume={36}, year={1935}, pages={127--150}, tue={IN BEZIT} } @misc{russ02, author={Russell, B.}, title={Letter to {F}rege}, year={1902}, howpublished={English translation in \cite{heij67}, pages 124--125}, tue={wis cbl 67 fro} } @book{russ03, author={Russell, B.}, title={The Principles of Mathematics}, year={1903}, publisher={Allen \&\ Unwin}, address={London}, tue={wis cbb 72 rus} } @article{russ08, author={Russell, B.}, title={Mathematical logic as based on the theory of types}, journal={American Journal of Mathematics}, volume={30}, year={1908}, note={Also in \cite{heij67}, pages 150--182}, tue={wis cbl 67 fro} } @book{russ19, author={Russell, B.}, title={Introduction to Mathematical Philosophy}, year={1919}, publisher={Allen \&\ Unwin}, address={London}, tue={centr mag cbd 60 rus} } %SSSS @article{sanc64, author={Sanchis, L.E.}, title={Types in Combinatory Logic}, volume={5}, journal={Notre Dame Journal of Formal Logic}, pages={161--180}, year={1964}, tue={IN BEZIT} } @article{schu60, author={Sch\"utte, K.}, year={1960}, journal={The Journal of Symbolic Logic}, volume={25}, title={Syntactical and Semantical Properties of Simple Type Theory}, pages={305--326}, tue={IN BEZIT} } @article{schw76, author={Schwichtenberg, H.}, year={1976}, title={Definierbare Funktionen im $\l$-Kalk\"ul mit Typen}, journal={Archief f\"ur Mathematische Logik}, volume={25}, pages={113-114} } @article{schw97, author={Schwichtenberg, H.}, title={Termination of permutative conversion inintuitionistic {G}entzen calculi}, note={To appear}, journal={Theoretical Computer Science}, year={1997}, } @techreport{sevepoll93, author="Severi, P. and Poll, E.", title={Pure Type Systems with definitions}, year={1993}, number={24}, institution={TUE Computing Science Notes}, address={Eindhoven University of Technology}, tue={IN BEZIT} } @inproceedings{sevepoll94, author="Severi, P. and Poll, E.", title="Pure Type Systems with Definitions", year={1994}, booktitle="Proceedings of LFCS'94 (LNCS {\bf 813})", pages={316--328}, publisher="Springer Verlag", address="New York", organization="LFCS'94, St.~Petersburg, Russia", editor={Nerode, A. and Matiyasevich, Yu.V.}, tue={} } @article{scho24, author={Sch\"onfinkel, M.}, year={1924}, title={\"{U}ber die {B}austeine der mathematischen {L}ogik}, journal={Mathematische Annalen}, volume={92}, note={Also in \cite{heij67}, pages 355--366}, tue={wis cbl 67 fro} } @book{sell87, author={Sells, P.}, year={1987}, title={Lectures on contemporary syntactic theories}, publisher={Center for the Study of Language and Information}, address={Stanford}, series={CSLI Lecture Notes {\bf 3}}, tue={KUB: LET E4 SELL 1985} } @misc{smitgerrmaaslaan93, author="Smit, J. and Gerritse, G. and Maassen, H. and Laan, T.", title={Kansrekening}, year={1993}, howpublished={Lecture notes, Catholic University Nijmegen}, note={Dutch}, tue={IN BEZIT} } @article{smytplot82, author = {Smyth, Michael B. and Plotkin, Gordon D.}, title = {The Category-theoretic Solution of Recursive Domain Equations}, volume = {11}, year = {1982}, journal = {SIAM Journal on Computing}, month = {November}, number = {4}, pages = {761--783} } @Book{stee84, author = "Guy L. {Steele Jr.}", title = "Common {L}isp: The Language", publisher = "Digital Press", year = "1984" } @phdthesis{spri95, author="Springintveld, J.", title="Algorithms for Type Theory", school="Department of Philosophy, Utrecht University", year="1995", tue={IN BEZIT} } @book{swar89, author={Swart, H.C.M. de}, year={1989}, title={Filosofie van de Wiskunde}, publisher={Martinus Nijhoff}, address={Leiden}, series={Serie Wetenschapsfilosofie}, note={Dutch}, tue={wm cbd 89 swa} } %TTTT @article{take53, author={Takeuti, G.}, year={1953}, title={On a generalized logic calculus}, journal={Japanese Journal of Mathematics}, volume={23}, pages={39--96}, tue={IN BEZIT} } @article{tars36, author={Tarski, A.}, title={Der {W}ahrheitsbegriff in den formalisierten {S}prachen}, journal={Studia Philosophica}, volume={1}, year={1936}, pages={261--405}, note={German translation by L. Blauwstein from the Polish original (193 3) with a postscript added}, tue={} } @techreport{terl89, author="Terlouw, J.", title={Een nadere bewijstheoretische analyse van {G}{S}{T}{T}'s}, institution={Department of Computer Science}, address={University of Nijmegen}, year={1989}, tue={...} } @misc{turn76, title={The {S}{A}{S}{L} language manual}, author={Turner, D. A.}, year=1976, address={University of St. Andrews} } @article{turn79, author={Turner, D.}, title={A new implementation technique for applicative languages}, journal={Software---Parctice and Experience}, volume=9, pages={31--49} } @incollection{turn81, author={Turner, D.}, title={The semantic elegance of functional languages}, booktitle={Proceedings of the ACM/MIT Conference on Functional languages and computer architecture}, year=1981, } @inproceedings{turn85, author={David A. Turner}, title={Miranda---a non-strict functional language with polymorphi c types}, booktitle={Functional programming languages and Computer Architec tures}, publisher={Springer Verlag}, year={1985}, series={Lecture Notes in Computer Science}, volume={201}, editor={J.P. Jouannaud} } %UUUU %VVVV @phdthesis{veld81, author={Veldman, W.H.M.}, title={Investigations in Intuitionistic Hierarchy Theory}, year={1981}, school={Catholic University Nijmegen}, tue={IN BEZIT} } @misc{veld84, author={Veldman, W.H.M.}, title={Modellentheorie}, year={1984}, howpublished={Lecture notes, Catholic University Nijmegen}, note={Dutch}, tue={IN BEZIT} } @misc{veld87, author={Veldman, W.H.M.}, year={1987}, title={Berekenbaar en Bewijsbaar (Recursietheorie)}, howpublished={Lecture Notes, Catholic University Nijmegen}, note={Dutch}, tue={IN BEZIT} } @misc{veld91, author={Veldman, W.H.M.}, year={1991}, title={Intu\"{\i}tionistische Wiskunde}, howpublished={Lecture Notes, Catholic University Nijmegen}, note={Dutch}, tue={IN BEZIT} } @techreport{vene93, author={Venema, Y.}, title={Meeting strength in substructural logics}, institution={OTS Working Papers}, year={1993}, tue={IN BEZIT reader categoriale grammatica} } @mastersthesis{vere93, author={Vereijken, J.J.}, title={Graph Grammars and Operations on Graphs}, year={1993}, school={Department of Computer Science, Leiden University}, tue={IN BEZIT} } @techreport{verh93, author={Verhoef, C.}, title={A general conservative extension theorem in process algebra}, institution={TUE Computing Science Notes}, address={Eindhoven University of Technology}, year={1993}, number={38}, tue={IN BEZIT} } @article{vrij85, author={Vrijer, R.~de }, journal={The Journal of Symbolic Logic}, title={A direct Proof of the Finite Developments Theorem}, volume={50}, pages={339--343}, number={2}, year={1985} } @article{vrij87, author={de Vrijer, R.}, title={Exactly estimating functionals and strong normalization}, journal={Indagationes Mathematicae}, volume={49}, pages={479--493}, year={1987}, } %WWWW @unpublished{wall93, author={Wallgren, J.}, title={Types in Logic Programming}, note={Draft version of end 1993}, tue={IN BEZIT} } @book{warn83, author={Warner, F. W.}, title={Foundations of differentiable manifolds and Lie groups}, year=1983, publisher={Springer}, address={Berlin}, series={ Graduate Texts in Mathematics, 94} } @book{weyl18, author={Weyl, H.}, title={Das Kontinuum}, year={1918}, publisher={Veit}, address={Leipzig}, note={German; also in: Das Kontinuum und andere Monographien, Chelsea P ub.Comp., New York, 1960}, tue={wis cad 60 kon} } @article{weyl46, author={Weyl, H.}, title={Mathematics and Logic: A brief survey serving as preface to a re view of ``{T}he {P}hilosophy of {B}ertrand {R}ussell''}, journal={American Mathematical Monthly}, year={1946}, tue={IN BEZIT} } @book{wild65, author="Wilder, R.L.", title="The Foundations of Mathematics", edition={second}, year={1965}, publisher={Robert E.~Krieger Publishing Company, Inc.}, address={New York}, tue={wis CBB 80 WIL} } @book{whit10, author="Whitehead, A.N. and Russell, B.", year={$1910^1$, $1927^2$}, title={Principia Mathematica}, publisher={Cambridge University Press}, tue={wis cbb 63 whi} } %XXXX %YYYY %ZZZZ %\input{extrawil.bib} @book{russwhit10, author={Russell, Bertrand A.W. and Whitehead, Alfred North}, title={Principia Mathematica}, publisher={Cambridge University Press}, year={1910--13} } @article{buch92, author={B. Buchberger}, title={Grobner Bases: An Introduction}, journal={Lecture Notes in Computer Science}, volume={623}, pages={378--??}, year={1992}, coden={LNCSD9}, issn={0302-9743}, bibdate={Mon May 13 11:46:24 MDT 1996}, acknowledgement={Nelson H. F. Beebe, Center for Scientific Computing, Department of Mathematics, University of Utah, Salt Lake City, UT 84112, USA, Tel: +1 801 581 5254, FAX: +1 801 581 4148, e-mail: \path beebe at math.utah.edu , URL: \path http://www.math.utah.edu/~beebe/} } @article{chur36, author={Alonzo Church}, title={An Unsolvable Problem of Elementary Number Theory}, journal={American Journal of Mathematics}, volume={58}, pages={354--363}, checked={No}, source={Barendregt HTCS bib}, year={1936} } @article{chur3233, author={Church, A.}, title={A set of postulates for the foundation of logic}, journal={Ann. of Math.}, volume={33}, pages={346--366}, year={1932}, note={Second paper with same title in Vol. 33, pages 839--864, of same journal} } @incollection{klee74, author={Kleene, S.C.}, title={Reminiscences of logicians. Reported by J. N. Crossley. With contributions by C. C. Chang, John Crossley, Jerry Keisler, Steve Kleene, Mike Morley, Vivienne Morley, Andrzej Mostowski, Anil Nerode, Gerald Sacks, Peter Hilton and David Lucy}, year={1975}, editor={Crossley, J.N.}, booktitle={Algebra and logic (Fourteenth Summer Res. Inst., Austral. Math. Soc., Monash Univ., Clayton, 1974)}, pages={1--62}, publisher={Springer}, address={Berlin}, series={Lecture Notes in Mathematics}, volume={450} } @article{turi37, author={Turing, A.M.}, title={Computability and lambda definability}, journal={J. Symbolic Logic}, volume={2}, year={1937}, pages={153--163} } @article{turi36, author={Alan M. Turing}, title={On Computable Numbers with an Application to the {E}ntscheidungsproblem}, journal={Proc. London Math. Soc. (2)}, volume={42}, year={1936}, pages={230--265}, annote={Hodges page 96 note 2.37; Reprinted in {\em The Undecidab le}.} } @article{skol23, author={Skolem, Thoralf}, title={Begr{\"u}ndung der elementaren {A}rithmetik durch die rekurrierende {D}enkweise ohne {A}nwendung scheinbarer {V}er{\"e}nderli chen mit unendlichem {A}usdehnungsbereich}, journal={Videnskapsselskapets skrifter, I. Matematisk-naturvidenskabelig klasse}, volume={6}, year={1923}, note={English translation in \citeasnoun{heij67}}, } @article{stat76, author={Statman, R.}, title={Typed lambda calculus}, journal={journal of}, year={1976} } @article {stat79, AUTHOR = {Statman, Richard}, TITLE = {The typed $\lambda $-calculus is not elementary recursive}, JOURNAL = {Theoret. Comput. Sci.}, FJOURNAL = {Theoretical Computer Science}, VOLUME = {9}, YEAR = {1979}, NUMBER = {1}, PAGES = {73--81}, ISSN = {0304-3975}, CODEN = {TCSDI}, } @article {stat79a, AUTHOR = {Statman, Richard}, TITLE = {Intuitionistic propositional logic is polynomial-space complete}, JOURNAL = {Theoret. Comput. Sci.}, FJOURNAL = {Theoretical Computer Science}, VOLUME = {9}, YEAR = {1979a}, NUMBER = {1}, PAGES = {67--72}, ISSN = {0304-3975}, CODEN = {TCSDI}, } @article {stat79b, AUTHOR = {Statman, R.}, TITLE = {Lower bounds on {H}erbrand's theorem}, JOURNAL = {Proc. Amer. Math. Soc.}, FJOURNAL = {Proceedings of the American Mathematical Society}, VOLUME = {75}, YEAR = {1979b}, NUMBER = {1}, PAGES = {104--107}, ISSN = {0002-9939}, CODEN = {PAMYAR}, } @incollection {stat80, AUTHOR = {Statman, Richard}, TITLE = {On the existence of closed terms in the typed $\lambda $-calculus. {I}}, BOOKTITLE = {{\rm in} \ncite{hindseld80}}, PAGES = {511--534}, PUBLISHER = {Academic Press}, ADDRESS = {London}, YEAR = {1980}, } @article {stat81, AUTHOR = {Statman, R.}, TITLE = {On the existence of closed terms in the typed $\lambda $\ calculus. {I}{I}. {T}ransformations of unification problems}, JOURNAL = {Theoret. Comput. Sci.}, FJOURNAL = {Theoretical Computer Science}, VOLUME = {15}, YEAR = {1981}, NUMBER = {3}, PAGES = {329--338}, ISSN = {0304-3975}, CODEN = {TCSDI}, } @Unpublished{stat80a, author = "Statman, Richard", title = "On the existence of closed terms in the typed $\lambda$-calculus. {I}{I}{I}", note = "Dept. of Mathematics, CMU, Pittsburgh, USA", OPTcrossref = "", OPTkey = "", year = "1980", OPTmonth = "", OPTannote = "" } @article {stat82, AUTHOR = {Statman, R.}, TITLE = {Completeness, invariance and $\lambda $-definability}, JOURNAL = {J. Symbolic Logic}, FJOURNAL = {The Journal of Symbolic Logic}, VOLUME = {47}, YEAR = {1982}, NUMBER = {1}, PAGES = {17--26}, ISSN = {0022-4812}, CODEN = {JSYLA6}, } @incollection {stat85, AUTHOR = {Statman, R.}, TITLE = {Equality between functionals revisited}, BOOKTITLE = {{\rm in} \ncite{harretal85}}, PAGES = {331--338}, PUBLISHER = {North-Holland}, ADDRESS = {Amsterdam}, YEAR = {1985}, } @book{vanHeijenoortJ:frofgs, author = {van Heijenoort, Jan}, title = {From {F}rege to {G}{\"o}del: a Source Book in Mathematical Logic, 1879--1931}, publisher = {Harvard University Press}, address = {Cambridge, MA}, libcongress = {67-10905}, isbn = {0 674 32450 1}, year = {1967}, reprinted = {1971, 1976}, pages = {xi+665} } @Book{hindseld80, author = "Seldin, J.P. and J.R. Hindley (Eds.)", title = "To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism", publisher = "Academic Press", year = "1980" } @incollection{gandturi80, author={Gandy, R.O.}, title={An early proof of normalization by {A.M. Turing}}, booktitle={To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism}, editors={Seldin, J.P. and J.R. Hindley}, publisher={Academic Press}, year={1980}, pages={453--455} } @article{davi82, title={Why {G{\"o}del} Didn't Have {Church's} Thesis}, author={Martin Davis}, pages={3--24}, journal={Information and Control}, month={jul / aug}, year={1982}, volume={54}, number={1/2} } @inproceedings{krei68, author={Kreisel, G.}, title={Church's thesis: A kind of reducibility axiom for constructive mathematics}, booktitle={Intuitionism and Proof Theory, Proc. Conf., Buffalo, N.Y., 1968}, pages={121--150}, publisher={North-Holland} } @article{troe98, author={Troelstra, A.~S.}, title={Marginalia on sequent calculi}, note={To appear}, journal={Studia Logica}, year={1998}, } @book{troeschw96, author={Troelstra, A.~S. and H. Schwichtenberg}, title={Basic Proof Theory}, publisher={Cambridge University Press}, address={Cambridge, UK}, year={1996} } @article{bohmbera85, key={Bohm85}, author={Corrado B{\"o}hm and Alessandro Berarducci}, title={Automatic Synthesis of Typed {$\Lambda$}-Programs on Term Algebras}, journal={Theoretical Computer Science}, volume={39}, year={1985}, pages={135--154}, source={From ergobib}, checked={Not checked}, complete={Incomplete} } @article{berabohm93, author={Alessandro Berarducci and Corrado Bohm}, title={A Self-Interpreter of Lambda Calculus Having a Normal Form}, journal={Lecture Notes in Computer Science}, volume={702}, pages={85--99}, year={1993}, coden={LNCSD9}, issn={0302-9743}, bibdate={Mon May 13 11:49:00 MDT 1996}, acknowledgement={Nelson H. F. Beebe, Center for Scientific Computing, Department of Mathematics, University of Utah, Salt Lake City, UT 84112, USA, Tel: +1 801 581 5254, FAX: +1 801 581 4148, e-mail: \path beebe at math.utah.edu , URL: \path http://www.math.utah.edu/~beebe/} } @incollection{bohm66, author={{B\"{o}hm}, Corrado}, title={The CUCH as a Formal and Description Language}, booktitle={Annual Review in Automatic Programming, Vol. 3}, editor={Richard Goodman}, publisher={Pergamon Press}, address={Oxford}, year={1963}, pages={179--197}, checked={11 March 1993} } @incollection{bohmgros66, author={C. B{\"o}hm and W. Gross}, title={Introduction to the {CUCH}}, booktitle={Automata Theory}, publisher={Academic Press}, editor={E.R. Caianiello}, address={New York}, year={1966}, pages={35--65} } @article{moge92, author={Mogensen, T. \AE.}, title={Theoretical pearls: Efficient self-interpretation in lambda calculus}, journal={Journal of Functional Programming}, volume={2}, number={3}, year={1992}, pages={345--364} } @article {baresmet96, AUTHOR = {Barendsen, Erik and Smetsers, Sjaak}, TITLE = {Uniqueness typing for functional languages with graph rewriting semantics}, NOTE = {Joint COMPUGRAPH/SEMAGRAPH Workshop on Graph Rewriting and Computation (Volterra, 1995)}, JOURNAL = {Math. Structures Comput. Sci.}, FJOURNAL = {Mathematical Structures in Computer Science. A Journal in the Applications of Categorical, Algebraic and Geometric Methods in Computer Science}, VOLUME = {6}, YEAR = {1996}, NUMBER = {6}, PAGES = {579--612}, ISSN = {0960-1295}, } @incollection{bare94, author={Barendregt, H.P.}, year={1994}, title={Discriminating coded lambda terms}, pages={141--151}, booktitle={From Universal Morphisms to Megabytes: A Baayen Space-Odyssey}, editor={Apt, K.R. and Schrijver, A.A. and Temme, N.M.}, publisher={CWI}, address={Kruislaan 413, 1098 SJ Amsterdam} } @article{bare95, author={Barendregt, H.P.}, title={Enumerators of lambda terms are reducing constructively}, journal={Annals of Pure and Applied Logic}, year={1995}, volume={73} } @proceedings{barenipk94, editor = {H. P. Barendregt and Tobias Nipkow}, booktitle = {Types for proofs and programs: international workshop {TYPES} '93, Nijmegen, The Netherlands, May 24--28, 1993: selected papers}, title = {Types for proofs and programs: international workshop {TYPES} '93, Nijmegen, The Netherlands, May 24--28, 1993: selected papers}, volume = {806}, publisher = {Spring{\-}er-Ver{\-}lag}, address = {Berlin, Germany~/ Heidelberg, Germany~/ London, UK~/ etc.}, pages = {383}, year = {1994} } @article {bare74, AUTHOR = {Barendregt, Henk}, TITLE = {Pairing without conventional restraints}, JOURNAL = {Z. Math. Logik Grundlagen Math.}, VOLUME = {20}, YEAR = {1974}, PAGES = {289--306}, } @article{bare91, author={Barendregt, H.P.}, title={Theoretical pearls: Self-interpretation in lambda calculus}, year={1991}, journal={Journal of Functional Programming}, volume={1}, number={2}, pages={229--233} } @book{hodg83, author={Hodges, A.}, title={The enigma of intelligence}, publisher={Unwin paperbacks}, address={London}, year=1983 } @article{miln78, author={Milner, R.}, title={A Theory of Type Polymorphism in Programming}, journal={Journal of Computer and System Sciences}, volume={17}, month={aug}, year={1978}, pages={348--375}, source={ergobib}, checked={Not checked} } @article{curr69, author={Curry, H.B.}, year=1969, title={Modified basic functionality in combinatory logic}, journal={Dialectica}, pages={83--92}, volume={23} } @article{back78, author={J. W. Backus}, title={Can Programming be liberated from the von Neuman style?}, journal={Comm. ACM}, year={1978}, volume={21}, pages={613--641} } @Book{appe92, author="Andrew W. Appel", title="Compiling with Continuations", publisher="Cambridge University Press", year=1992 } @Article{clinrees91, xeditor="William Clinger and Jonathan Rees (editors)", author="William Clinger and Jonathan Rees (editors)", title="Revised${}^4$ Report on the Algorithmic Language {S}cheme", journal="LISP Pointers", volume="IV", number=3, pages="1-55", month="July-September", year=1991 } @Unpublished{plot85, author = "Plotkin, G.", title = "Personal communication", note = "email", OPTcrossref = "", OPTkey = "", year = "1985?", OPTmonth = "", OPTannote = "" } @InProceedings{reyn74, author="John C. Reynolds", title="On the Relation between Direct and Continuation Semantics" , booktitle="2nd Colloquium on Automata, Languages and Programming", year=1974, editor="Jacques Loeckx", series=LNCS, number=14, pages="141-156", OPTpublisher=S-V, address="Saarbr{\"{u}}cken, West Germany", month=Jul } @Article{reyn93, author="John C. Reynolds", title="The Discoveries of Continuations", pages="233-247", journal="LISP and Symbolic Computation", year=1993, volume=6, number="3/4", month=Dec } @TechReport{stee78, author="Guy L. {Steele Jr.}", title="RABBIT: A Compiler for {S}CHEME", institution="Artificial Intelligence Laboratory, Massachusetts Institute of Technology", year=1978, number="AI-TR-474", address="Cambridge, Massachusetts", month=May } @Book{milntoftharp90, author="Robin Milner and Mads Tofte and Robert Harper", title="The Definition of {S}tandard {ML}", publisher="The MIT Press", year=1990 } @Article{mogg91, author="Eugenio Moggi", title="Notions of Computation and Monads", journal="Information and Computation", year=1991, volume=93, pages="55-92" } @book{land60, author={Landau, E.}, title={Grundlagen der Analysis}, publisher={Chelsea Publishing Company}, year={1960}, edition={3-rd edition} } @article{land65, author={Peter J. Landin}, title={A correspondence between {ALGOL} 60 and {Church}'s lambda notation}, year={1965}, journal={Communications of the ACM}, volume={8}, pages={89--101,158--165} } @article{land64, author={Peter J. Landin}, title={The Mechanical Evaluation of Expressions}, journal={The Computer Journal}, volume={6}, number={4}, pages={308--320}, month={jan}, year={1964} } @phdthesis{wads71, author={C. Wadsworth}, title={Semantics and Pragmatics of the Lambda-Calculus}, school={University of {Oxford}}, year={1971}, type={{D.Phil} Thesis}, address={Programming Research Group, Oxford, {U.K.}} } @incollection{scot80a, author={Dana S. Scott}, title={Relating Theories of the {$\lambda$}-Calculus}, checked={Yes}, pages={403--450}, crossref={PierceBC,CurryFestschrift} } @article{koym82, author={Koymans, C.P.J.}, key={Koymans 82}, title={Models of the lambda calculus}, journal={Information and Control}, volume={52}, number={3}, year={1982}, pages={306-323} } @book{leeu90, booktitle = {Handbook of Theoretical Computer Science}, editor = {J. Van Leeuwen}, publisher = {North-Holland, MIT-Press}, title = {Handbook of Theoretical Computer Science}, year = {1990}, volume={A, B}, } @incollection{guntscot90, author={C. A. Gunter and D. S. Scott}, booktitle={Handbook of Theoretical Computer Science}, crossref={leeu90}, title={Semantic Domains}, pages={633--674}, volume={B} } @incollection{scot80, author={D.S. Scott}, title={Lambda Calculus: Some Models, Some Philosophy}, booktitle={The Kleene Symposium}, editor={J. Barwise and H. J. Keisler and K. Kunen}, publisher={North-Holland Publishing Company}, year={1980}, pages={223--265} } %%%%%ZZZZZ @article{zuck74, author={Zucker, J.}, title={Cut--elimination and normalization}, journal={Annals of Mathematical Logic}, volume={7}, pages={1--112}, year={1974}, } @phdthesis{hugh84, title={The design and implementation of programming languages}, year=1984, author={Hughes, R. J. M.}, school={University of Oxford} } @article{hugh89, author={R. J. M. Hughes}, title={Why Functional Programming Matters}, journal={The Computer Journal}, volume={32}, number={2}, pages={98--107}, month={apr}, year={1989}, } @book{hend80, author={P. Henderson}, title={Functional Programming: Application and Implementation}, year={1980}, publisher={Prentice-Hall}, address={Englewood Cliffs, New Jersey} } @article{john84, author={T. Johnsson}, title={Efficient Compilation of Lazy Evaluation}, booktitle={Proceedings of the ACM SIGPLAN'84 Symposium on Compiler Con struction}, journal={SIGPLAN Notices}, year={1984}, month={June}, volume={19}, number={6}, publisher={ACM Press}, organization={ACM}, pages={58-69} } @proceedings{bezegroot93, title={Typed Lambda Calculi and Applications, TLCA'93}, year={1993}, editor={Bezem, M. and Groote, J.F.}, series={Lecture Notes in Computer Science}, number={664}, publisher={Springer Verlag}, tue={IN BEZIT}, address={Berlin} } @incollection{paul93, author={Paulin-Mohring, C.}, year=1994, crossrefer={bezegroot93}, title={Inductive definitions in the system Coq; rules and properties}, booktitle={\citeasnoun{bezegroot93}}, pages={328--345}, series={Lecture Notes in Computer Science}, number={664}, publisher={Springer Verlag}, tue={IN BEZIT}, address={Berlin} } @book{plaseeke93, author={Eekelen, M.C.J.D.~van and M.J. Plasmeijer}, title={Functional Programming and Parallel Graph Rewriting}, publisher={Addison-Wesley}, address={Reading, Massachusetts}, year={1993} } @book{Pey87, author = {S.L. Peyton Jones}, title = {The Implementation of Functional Programming Languages}, publisher = {Prentice-Hall}, year = {1987} } @inproceedings{peytwadl93, author={S. L. Peyton Jones and P. Wadler}, title={Imperative functional programming}, booktitle={Conference record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Charleston, South Carolina, January 10-13, 1992}, publisher={ACM Press}, pages={71--84}, month={}, year={1993}, bibdate={Thu Dec 14 18:49:37 MST 1995}, acknowledgement={Nelson H. F. Beebe, Center for Scientific Computing, Department of Mathematics, University of Utah, Salt Lake City, UT 84112, USA, Tel: +1 801 581 5254, FAX: +1 801 581 4148, e-mail: \path beebe at math.utah.edu , URL: \path http://www.math.utah.edu/\verb+~+beebe/}, affiliation={Dept. of Comput. Sci., Glasgow Univ., UK}, classification={C6110 (Systems analysis and programming); C6140D (High level languages)}, confdate={10-13 Jan. 1993}, conflocation={Charleston, SC, USA}, confsponsor={ACM}, keywords={Imperative functional programming; Monads; Input/output; Purely functional language; Mixed-language working; In-place array updates}, language={English}, pubcountry={USA}, thesaurus={Functional programming; High level languages} } @article{huda94, author={P. Hudak and S. Peyton Jones and P. Walder and B. Boutel and J. Fairbairn and J. Fasel and M. M. Guzman and K. Hammond and J. Hughes and T. Johnsson and D. Kieburtz and R. Nikhil and W. Partain and J. Peterson}, title={Report on the programming language {Haskell}: a non-strict, purely functional language (Version 1.2)}, journal={ACM SIG{\-}PLAN Notices}, volume={27}, number={5}, pages={Ri--Rx, R1--R163}, month={may}, year={1992}, coden={SINODQ}, issn={0362-1340}, bibdate={Sat Dec 16 15:47:40 1995} } @book{gord94, author={Andrew D. Gordon}, title={Functional programming and {I}nput/{O}utput}, series={Distinguished {D}issertations in {C}omputer {S}cience}, year={1994}, publisher={{C}ambridge {U}niversity {P}ress} } @incollection{gent35, author={Gentzen, Gerhard}, title={Investigations into Logical Deduction}, editor={Szabo, M. E.}, booktitle={The Collected Papers of Gerhard Gentzen}, publisher={North-Holland}, seriestitle={Studies in the Foundations of Mathematics}, year={1969}, isbn={0 7204 2254 X}, libcong={71-97201}, qmwlib={QA4 GEN} } @techreport{luopoll92, author={Zhaohui Luo and Robert Pollack}, title={The {LEGO} Proof Development System: A User's Manual}, institution={University of Edinburgh}, month={may}, year={1992}, number={ECS-LFCS-92-211}, keywords={misc}, ??={http://www.dcs.ed.ac.uk/packages/lego/} } @article{coqu88, key={Coquand88}, author={Thierry Coquand and G{\'e}rard Huet}, title={The {Calculus of Constructions}}, journal={Information and Computation}, volume={76}, number={2/3}, month={February/March}, year={1988}, pages={95--120}, source={ergobib}, ??={http://pauillac.inria.fr/~coq/coq-eng.html} } @phdthesis{jutt77, author={{L.S. van Benthem} Jutting}, title={Checking {Landau's} ``{Grundlagen}'' in the {AUTOMATH} System}, school={Eindhoven University of Technology}, year={1977}, keywords={Automath} } @article{jutt93, title={Typing in Pure Type Systems}, author={L. S. van Benthem Jutting}, pages={30--41}, journal={Information and Computation}, month={jul}, year={1993}, volume={105}, number={1} } @incollection{juttmckipoll93, author={{L.S. van Benthem} Jutting and James McKinna and Robert Pollack}, title={Checking Algorithms for {P}ure {T}ype {S}ystems}, booktitle={Proceedings of the International Workshop on Types for Proofs and Programs}, month={may}, address={Nijmegen, The Netherlands}, editor={Henk Barendregt and Tobias Nipkow}, pages={19--61}, publisher={Springer-Verlag LNCS 806}, year={1993}, keywords={misc} } @inproceedings{leiv83, author={Leivant, Daniel}, title={Reasoning About Functional Programs and Complexity Classes Associated with Type Disciplines}, booktitle={24th Annual Symposium on Foundations of Computer Science}, organization={IEEE}, place={Tucson, Arizona}, dates={November 7--9}, year={1983}, pages={460--469}, checked={5 July 1990} } @INPROCEEDINGS{baresmet93 , AUTHOR ={Barendsen, E. and J.E.W. Smetsers} , TITLE ={Conventional and Uniqueness Typing in Graph Rewrite Systems (extended abstract)} , CROSSREF ={shya93} , BOOKTITLE ={\ncite{shya93}} , PAGES ={41--51} } @Article{Reynolds:LaSC93, author = "John C. Reynolds", title = "The Discoveries of Continuations", pages = "233-247", journal = "LISP and Symbolic Computation", year = 1993, volume = 6, number = "3/4", month = Dec } @TechReport{Steele:78, author = "Guy L. {Steele Jr.}", title = "RABBIT: A Compiler for {S}CHEME", institution = "Artificial Intelligence Laboratory, Massachusetts Institute of Technology", year = 1978, number = "AI-TR-474", address = "Cambridge, Massachusetts", month = May } @book{algo68, editor = {van Wijngaarden, A. and Mailloux, B.J. and Peck, J.E.L. and Koster, C.H.A. and Sintzoff, M. and C.H.~Lindsey and Meertens, L.G.L.T. and Fisker, R.G.}, title = {Revised Report on the Algorithmic Language {{\sc Algol~68}}}, publisher = {Springer Verlag, Berlin}, year = 1976 } %%%%%%%%%AAAA @article{acke28, author={Ackermann, W.}, title={Zum {H}ilbertschen {A}ufbau der {r}eellen {Z}ahlen}, journal={Mathematische Annalen}, year=1928, volume=99, pages={118--133} } @inproceedings{acze78, author={Aczel, P.}, title={The type theoretic interpretation of constructive set theory}, booktitle={Logic Colloquium '77}, note={Studies in Logic and the Foundations of Mathematics {\bf 96}}, editor="Macintyre, A. and Pacholski, L. and Paris, J.", publisher={North-Holland}, address={Amsterdam}, year={1978}, tue={wis cbl 71 log} } @inproceedings{acze80, author={Aczel, P.}, title={Frege structures and the notion of proposition, truth and set}, booktitle={The Kleene Symposium}, note={Studies in Logic and the Foundations of Mathematics {\bf 101}}, editor="Barwise, J. and Keisler, H. and Kunen, K.", publisher={North-Holland}, address={Amsterdam}, year={1980}, tue={wis cbn 80 kle} } @article{ajdu35, author={Ajdukiewicz, K.}, title={Die syntaktische {K}onnexit\"at}, journal={Studia Philosophica}, volume={1}, pages={1--27}, year={1935}, note={in German; English translation in \cite{mcca67}}, tue={Zie mcca67} } @mastersthesis{aleb94, author={van Alebeek, E.}, title={Isomorfie van beslisbare en opsombare ondergroepen van $(\q,+)$} , school={Department of Mathematics, Catholic University Nijmegen}, year={1994}, note={Dutch}, tue={IN BEZIT} } @inproceedings{aspicomp96, author = {D. Aspinall and A. Compagnoni}, title = {Subtyping Dependent Types}, editor = {E. Clarke}, pages = {86--97}, booktitle = {Proceedings of the 11th Annual Symposium on Logic in Computer Science}, year = {1996}, publisher = {IEEE Computer Society Press}, address = {New Brunswick, New Jersey}, month = {jul}, keywords = {LF} } %%%%%%BBBB @techreport{baetmauw94, author="Baeten, J.C.M. and Mauw, S.", title={Delayed Choice: An Operator for Joining Message Sequence Charts} , year={1994}, number={35}, institution={TUE Computing Science Reports}, address={Eindhoven University of Technology}, tue={IN BEZIT} } @book{bare84, author={Barendregt, H.P.}, title={The Lambda Calculus: its Syntax and Semantics}, year={1984}, edition={revised}, publisher={North-Holland}, address={Amsterdam}, tue={IN BEZIT} } @article{barebunddekk93, author="Barendregt, H.P. and Bunder, M. and Dekkers, W.", title={Systems of Illative Combinatory Logic complete for first order propositional and predicate calculus}, year={1993}, journal={The Journal of Symbolic Logic}, volume={58}, number={3}, pages={89--108}, tue={IN BEZIT} } @book{barwmoss96, author="Barwise, J. and Moss, L.", title="Vicious Circles", year={1996}, address={Stanford}, publisher={CSLI Publications}, tue={wis ...} } @book{bees80, author={Beeson, M.J.}, title={Foundations of Constructive Mathematics}, publisher={Springer}, year={1980}, address={Berlin} } @book{benaputn83, editor="Benacerraf, P. and Putnam, H.", title={Philosophy of Mathematics}, publisher={Cambridge University Press}, year={1983}, edition={second}, tue={wis cbd 83 phi} } @article{bent78, author="van Benthem, J.F.A.K.", title="Four Paradoxes", year={1978}, journal="Journal of Philosophical Logic", volume="7", pages="49--72", tue={IN BEZIT} } @book{bent91, author={van Benthem, J.F.A.K.}, title={Language in Action: Categories, Lambdas and Dynamic Logic}, publisher={North-Holland}, year={1991}, series={Studies in Logic and the Foundations of Mathematics {\bf 130}}, address={Amsterdam}, tue={IN BEZIT} } @techreport{btjt81, author={van Benthem Jutting, L.S.}, title={Description of {A}{U}{T}-68}, year={1981}, number={12}, institution={Eindhoven University of Technology}, note={also in \cite{nedegeuvvrij94}}, tue={IN BEZIT} } @article{jutt93, title={Typing in Pure Type Systems}, author={L.S. van Benthem Jutting}, pages={30--41}, journal={Information and Computation}, month={jul}, year={1993}, volume={105}, number={1} } @incollection{juttmckipoll93, author={L.S. van Benthem Jutting and J. McKinna and R. Pollack}, title={Checking Algorithms for {P}ure {T}ype {S}ystems}, booktitle={Proceedings of the International Workshop on Types for Proofs and Programs}, month={may}, address={Nijmegen, The Netherlands}, editor={Henk Barendregt and Tobias Nipkow}, pages={19--61}, publisher={Springer}, address={Berlin and New York}, volume={58}, series={Lecture Notes in Computer Science}, year={1993}, keywords={misc} } @techreport{bera88, author={Berardi, S.}, title={Towards a mathematical analysis of the {C}oquand-{H}uet calculus of constructions and the other systems in {B}arendregt's cube}, year={1988}, institution={Dept. of Computer Science, Carnegie-Mellon University and Dipartimento Matematica, Universita di Torino}, tue={...} } @phdthesis{bera90, author={Berardi, S.}, title={Type Dependence and Constructive Mathematics}, year={1990}, school={Dipartimento Matematica}, address={Universit\`a di Torino}, tue={...} } @techreport{berabezecoqu94, author="Berardi, S. and Bezem, M.A. and Coquand, T.", title={On the computational content of the Axiom of Choice}, year={1994}, number={116}, institution={Department of Philosophy, Utrecht University}, tue={IN BEZIT} } @book{bergklopmidd89, author="Bergstra, J.A. and Klop, J.W. and Middeldorp, A.", title={Termherschrijfsystemen}, publisher={Kluwer Programmatuurkunde}, year={1989}, note={Dutch}, tue={wis dbn 89 ber} } @book{beth59, author={Beth, E.W.}, title={The Foundations of Mathematics}, publisher={North-Holland}, year={1959}, series={Studies in Logic and the Foundations of Mathematics}, address={Amsterdam}, tue={wis cbb 59 bet} } @mastersthesis{blee95, author={Bleeker, A.}, title={An Approach to Image Retrieval}, year={1995}, school={Katholieke Universiteit Nijmegen/Universit\`a di Padova}, tue={IN BEZIT} } @mastersthesis{bloo93, author={Bloo, R.}, title={Over de begrippen gefundeerd en verstrooid}, year={1993}, school={Department of Mathematics, Catholic University Nijmegen}, note={Dutch}, tue={IN BEZIT} } @techreport{bloo95, author={Bloo, R.}, title={Preservation of Strong Normalisation for Explicit Substitution}, institution={TUE Computing Science Notes}, address={Eindhoven University of Technology}, number={8}, year={1995}, month={mar}, tue={IN BEZIT} } @techreport{blookamanede94, author="Bloo, R. and Kamareddine, F. and Nederpelt, R.", title={Beyond $\beta$-Reduction in {C}hurch's $\lambda{\rightarrow}$}, institution={TUE Computing Science Notes}, address={Eindhoven University of Technology}, number={20}, year={1994}, month={apr}, tue={IN BEZIT} } @techreport{blookamanede94a, author="Bloo, R. and Kamareddine, F. and Nederpelt, R.", title={The $\lambda$-cube with classes of terms modulo conversion}, institution={TUE Computing Science Reports}, address={Eindhoven University of Technology}, number={46}, year={1994}, tue={IN BEZIT} } @techreport{blookamanede94b, author={Bloo, R. and Kamareddine, F. and Nederpelt, R.}, title={On {$\Pi$}-conversion in Type Theory}, institution={TUE Computing Science Reports}, address={Eindhoven University of Technology}, number={47}, year={1994}, tue={IN BEZIT} } @techreport{blookamanede94c, author={Bloo, R. and Kamareddine, F. and Nederpelt, R.}, title={The {B}arendregt {C}ube with {D}efinitions and {G}eneralised {R} eduction}, institution={TUE Computing Science Reports}, address={Eindhoven University of Technology}, number={34}, year={1994}, note={Also as Technical Report 8, University of Glasgow, Computing Science Department, 1994. To be published in Information and Computation}, tue={IN BEZIT} } @article{blookamanede95, author={Kamareddine, F. and Bloo, R. and Nederpelt, R.}, title={Definitions and {$\Pi$}-conversion in Type Theory}, year={1995}, journal={Submitted}, tue={Copie IN BEZIT} } @article{blookamanede96, author={Bloo, R. and Kamareddine, F. and Nederpelt, R.}, title={The {B}arendregt {C}ube with {D}efinitions and {G}eneralised {R}eduction}, year={1996}, journal={{I}nformation and {C}omputation}, volume={126}, number={2}, pages={123--143}, tue={IN BEZIT} } @inproceedings{bohmpipeguer94, author = {C. B\"ohm and A. Piperno and S. Guerrini}, title = {lambda-definition of function(al)s by normal forms}, journal = {Lecture Notes in Computer Science}, publisher={Springer}, address={Berlin}, volume = {788}, booktitle={ESOP'94}, editor={D. Sanella}, pages = {135--154}, year = {1994} } @phdthesis{borg94, author={Borghuis, V.A.J.}, title={Coming to Terms with Modal Logic: On the interpretation of modal ities in typed $\lambda$-calculus}, school={Technische Universiteit Eindhoven}, year={1994}, tue={IN BEZIT} } @phdthesis{boum93, author={Bouma, G.}, title={Nonmonotonicity and Categorial Unification Grammar}, school={Rijksuniversiteit Groningen}, year={1993}, tue={hfst. 1-3 in reader categoriale grammatica IN BEZIT} } @mastersthesis{bran95, author={Brands, J.}, title={Spelen met 0-1 wetten}, school={Department of Mathematics, Catholic University Nijmegen}, year={1995}, note={Dutch}, tue={IN BEZIT} } @mastersthesis{bron94, author={Bron, I.G.L.}, title={Benaderen van looptijden voor uittredingen die zich met zeer kle ine kans voordoen}, school={Department of Mathematics, Catholic University Nijmegen}, year={1994}, note={Dutch}, tue={IN BEZIT} } @phdthesis{brou07, author={{B}rouwer, L.E.J.}, title={Over de Grondslagen der Wiskunde}, school={Universiteit van Amsterdam}, year={1907}, note={Dutch; English translation in \cite{heyt75}}, tue={collected works: wis cae 75 bro; {van} Dalen (ed): wis cbb 81 bro} } @article{brou18, author={Brouwer, L.E.J.}, title={Begr\"undung der {M}engenlehre unabh\"angig vom logischen {S}atz vom ausgeschlossenen {D}ritten}, journal={KNAW Verhandelingen}, year={1918}, volume={12}, number={5}, note={German; also in \cite{heyt75}}, tue={collected works: wis cae 75 bro} } @techreport{brui68, author={de Bruijn, N.G.}, title="{A}{U}{T}{O}{M}{A}{T}{H}, a language for mathematics", year={1968}, institution={T.H.-Reports}, number={68-{W}{S}{K}-05}, address={Eindhoven University of Technology}, tue={wis ARC 01 EUT} } @booklet{brui90, author={de Bruijn, N.G.}, title="Reflections on {A}utomath", year={1990}, address={Eindhoven University of Technology}, note={Also in \cite{nedegeuvvrij94}, pp 201--228}, tue={IN BEZIT} } @techreport{brunkatokoymmauw93, author="Brunekreef, J. and Katoen, J.-P. and Koymans, R. and Mauw, S.", title={Design and Analysis of Dynamic Leader Election Protocols in Broa dcast Networks}, year={1993}, number={37}, institution={TUE Computing Science Notes}, address={Eindhoven University of Technology}, tue={IN BEZIT} } @article{bura97, author={Burali-Forti, C.}, title={Una questione su i numeri transfiniti}, year={1897}, journal={Rendiconti del Corcolo Matematico di Palermo}, volume={11}, note={English translation in \cite{heij67}, pages 104--112} } @article{burg86, author={Burgess, J.P.}, title={The Truth is Never Simple}, journal={Journal of Symbolic Logic}, volume={51}, pages={663--681}, year={1986}, tue={IN BEZIT} } @book{buszmarcbent88, editor="Buszkowski, W. and Marciszewski, W. and van Benthem, J.", title={Categorial Grammar}, publisher={John Benjamins}, year={1988}, series={Linguistic \&\ Literary Studies in Eastern Europe {\bf 25}}, address={Amsterdam}, tue={IPO-bibliotheek XF 88} } %CCCC @book{carn29, author={Carnap, R.}, title={Abriss der Logistik}, year={1929}, publisher={Springer}, address={Berlin and New York}, address={Wien} } @book{carn65, author={Carnap, R.}, title={Foundations of Logic and Mathematics}, series={International Encyclopedia of Unified Science}, year={1965}, publisher={University of Chicago Press}, tue={wis cbb 65 car} } @article{chieturn88, author="Chierchia, G. and Turner, R.", title="Semantics and property theory", journal="Linguistics and Philosophy", volume="11", pages="261--302", year={1988}, tue={---} } @book{chur56, author={Church, A.}, title={Introduction to Mathematical Logic}, publisher={Princeton University Press}, year={1956}, tue={wis cbk 56 chu} } @article{chur76, author={Church, A.}, title={Comparison of {R}ussell's Resolution of the Semantic Antinomies with that of {T}arski}, journal={The Journal of Symbolic Logic}, year={1976}, volume={41}, pages={747--760}, tue={IN BIBLIOTHEEK WSK} } @book{consETAL86, author={Constable et al., R.L.}, title="Implementing Mathematics with the Nuprl Proof Development System", year={1986}, publisher={Prentice-Hall}, address={New Jersey}, tue={DGR 6 IMP} } @phdthesis{coqu85, author={Coquand, T.}, title={Une th\'eorie des constructions}, year={1985}, school={Universit\'e Paris VII}, address={Th\`ese de troisi\`eme cycle}, tue={...} } @inproceedings{coqu86, author={Coquand, T.}, title={An Analysis of {G}irard's Paradox}, booktitle={Proceedings of the Symposium on Logic in Computing Science}, year={1986}, address={Cambridge, Massachusetts}, organization={IEEE}, tue={IN BEZIT} } @article{coquhuet88, author="Coquand, T. and Huet, G.", title="The Calculus of Constructions", journal="Information and Computation", year={1988}, volume={76}, pages={95--120}, note={Available at URL :\\ http://pauillac.inria.fr/~coq/coq-eng.html}, tue={...} } @article{curi86a, title = {Categorical Combinators}, author = {P.-L. Curien}, pages = {188--254}, journal = {Information and Control}, month = {apr / may / jun}, year = {1986}, volume = {69}, number = {1--3} } @article{curr29, author={Curry, H.B.}, year={1929}, title={An Analysis of Logical Substitution}, journal={American Journal of Mathematics}, volume={51}, pages={363--384}, tue={IN BEZIT} } @article{curr30, author={Curry, H.B.}, year={1930}, title={Grundlagen der kombinatorischen {L}ogik}, journal={American Journal of Mathematics}, volume={52}, pages={509--536, 789--834}, note={German}, tue={IN BEZIT} } @book{curr63, author={Curry, H.B.}, year={1963}, title={Foundations of Mathematical Logic}, publisher={McGraw-Hill Book Company, Inc.}, series={McGraw-Hill Series in Higher Mathematics}, tue={wis cbk 63 cur} } @book{currhindseld72, author="Curry, H.B. and Hindley, J.R. and Seldin, J.P.", year={1972}, title={Combinatory Logic}, publisher={North-Holland}, address={Amsterdam}, volume={II}, series={Studies in Logic and the Foundations of Mathematics}, tue={wis cbk 72 cur} } %DDDD @inproceedings{daal73, author="van Daalen, D.T.", title="A description of {A}utomath and some aspects of its language theory", editor="Braffort, P.", booktitle="Proceedings of the Symposium APLASM", year="1973", volume="I", note="Also in \cite{nedegeuvvrij94}", tue={IN BEZIT} } @phdthesis{daal80, author={van Daalen, D.T.}, title="The Language Theory of Automath", year="1980", school="Eindhoven University of Technology", tue="wis cbk 80 daa" } @book{dale78, author={van Dalen, D.}, title={Filosofische grondslagen van de wiskunde}, publisher={Van Gorcum}, year={1978}, address={Assen, Amsterdam}, note={Dutch}, tue={IN BEZIT} } @book{dale81, editor={van Dalen, D.}, title={Over de Grondslagen der Wiskunde}, publisher={Mathematisch Centrum}, year={1981}, address={Amsterdam}, note={Dutch; L.E.J. Brouwers' Thesis together with unpublished fragme nt s, correspondence with D.J. Korteweg, review by G. Mannoury, and an introduction} , tue={cbb 81 bro} } @article{dalefreukrol81, author="van Dalen, D. and Freudenthal, H. and Krol, G.", title={De wiskundige {B}rouwer en de eenzaamheid van het gelijk}, journal={Vrij Nederland}, year={1981}, month={feb}, note={Dutch}, tue={caz 81 dal} } @techreport{damsgrumgert94, author="Dams, D. and Grumberg, O. and Gerth, R.", title={Abstract Interpretation of Reactive Systems: Abstractions Preser ving $\al$CTL*, $\er$CTL* and CTL*}, year={1994}, number={24}, institution={TUE Computing Science Notes}, address={Eindhoven University of Technology}, tue={IN BEZIT} } @article{davi73, author={Davis, M.}, title={Hilbert's tenth problem is unsolvable}, journal={American Mathematical Monthly}, volume=80, year=1973, pages={233--269} } @book{dede72, author="Dedekind, R.", title={Stetigkeit und irrationale Zahlen}, address={Braunschweig}, year={1872}, publisher={{}}, tue={...} } @unpublished{dekk93, author={Dekkers, W.}, title={Lambda calculus en herschrijfsystemen}, note={Lecture notes W7-HL, Catholic University of Nijmegen}, year={1993}, tue={IN BEZIT} } @proceedings{dezaplot95, editor="Dezani-Ciancaglini, M. and Plotkin, G.", title={Second International Conference on Typed Lambda Calculi and Applications, TLCA'95}, year={1995}, series={Lecture Notes in Computer Science}, number={902}, publisher={Springer}, tue={IN BEZIT}, address={Berlin and New York} } @techreport{dose90, author={Dosen, K.}, title={A Brief Survey of Frames for the {L}ambek Calculus}, institution={Konstanzer Berichte zur Logik und Wissenschaftstheorie}, year={1990}, number={5}, tue={IN BEZIT reader categoriale grammatica} } @techreport{dowe91, author={{Dowek et al.}, G.}, title={The {C}oq {P}roof {A}ssistant {V}ersion 5.6, {U}sers {G}uide}, year={1991}, institution={INRIA}, number={134}, address={Le Chesney} } %EEEE %FFFF @inproceedings{fefe75, author={Feferman, S.}, booktitle={Proof Theory Symposium}, year={1975}, editor={J.H. Diller and G.H. M\"uller}, title={A language and axioms for explicit mathematics}, publisher={Springer}, series={Lecture Notes in Mathematics}, volume={500}, address={Berlin}, pages={87--139}, } @inproceedings{fefe79, author={Feferman, S.}, booktitle={Logic Colloquium '78}, year={1979}, editor={Boffa, M. and van Dalen, D. and McAloon, K}, title={Constructive Theories of Functions and Classes}, publisher={North Holland}, address={Amsterdam}, pages={159--224}, tue={IN BEZIT} } @article{fefe84, author={Feferman, S.}, title={Toward useful type-free theories {I}}, journal={Journal of Symbolic Logic}, volume={49}, year={1984}, pages={75--111}, tue={IN BEZIT} } @article{fefe95, author={Feferman, S.}, title={Definedness}, journal={Erkentniss}, volume={43}, year={1995}, pages={295--320}, } @book{frae27, author={Fraenkel, A.}, title={Zehn Vorlesungen \"uber die Grundlegung der Mengenlehre}, year={1927}, publisher={B.G. Teubner}, address={Leipzig, Berlin}, series={Wissenschaft und Hypothese, Band XXXI}, note={German}, tue={ruu wis fr 01 1} } @book{frae28, author={Fraenkel, A.}, title={Einleitung in die Mengenlehre}, year={1928}, publisher={Springer}, address={Berlin and New York}, series={Die Grundlehren der mathematischen Wissenschaften in Einzeldars tellungen mit besonderer Ber\"ucksichtigung der Anwendungsgebiete, Band IX}, edition={third}, note={German}, tue={ruu wis fr 01 2a} } @book{fraebarhlevy73, author="Fraenkel, A.A. and Bar-Hillel, Y. and Levy, A.", title={Foundations of Set Theory}, publisher={North Nolland}, year={1973}, series={Studies in Logic and the Foundations of Mathematics 67}, address={Amsterdam}, edition={second}, tue={wks cbf 58 fra} } @book{freg79, author={Frege, G.}, title={Begriffschrift, eine der arithmetischen nachgebildete Formelspra che des reinen Denkens}, publisher={Nebert}, address={Halle}, year={1879}, note={Also in \cite{heij67}, pages 1--82}, tue={in wis cbl 67 fro} } @book{freg84, author={Frege, G.}, title={Grundlagen der Arithmetik}, address={Breslau}, publisher={{}}, year={1884}, note={(also in \cite{benaputn83})}, tue={in wis cbd 83 phi} } @book{freg92, author={Frege, G.}, title={Grundgesetze der Arithmetik, begriffsschriftlich abgeleitet}, address={Jena}, publisher={{}}, year={1892}, volume={I}, note={Reprinted 1962 (Olms, Hildesheim)}, tue={...} } @book{freg03, author={Frege, G.}, title={Grundgesetze der Arithmetik, begriffsschriftlich abgeleitet}, address={Jena}, publisher={Pohle}, year={1903}, volume={II}, note={Reprinted 1962 (Olms, Hildesheim)}, tue={...} } %GGGG @book{gamu91, author={Gamut, L.~T.~F.}, year={1991}, title={Logic, Language and Meaning}, publisher={Chicago University Press}, address={Chicago} } @inproceedings{gand77, author={Gandy, R.O.}, title={The Simple Theory of Types}, booktitle={Logic Colloquium '76}, publisher={North-Holland}, editor="Gandy, R.O. and Hyland, J.M.E.", year={1977}, pages={173--181}, address={Amsterdam}, note={Studies in Logic and the Foundations of Mathematics {\bf 87}}, tue={wis cbl 71 log} } @incollection{gand80a, author={Gandy, R.O.}, title={Church's {T}hesis and principles for mechanisms}, editors={Barwise, J. and Keisler, H.J. and Kunen, K.}, booktitle={The Kleene Symposium}, publisher={North-Holland Publishing Company}, year={1980}, address={Amsterdam}, pages={123--148} } @article{gent30, author={Gentzen, G.}, title={Die Widerspruchsfreiheit der {S}tufenlogik}, journal={Mathematische Zeitschrift}, year={1930}, volume={41}, pages={357--366}, note={German}, tue={IN BEZIT} } @booklet{gerh90, author={{Gerhardt, editor}, C.I.}, title={Die Philosophischen {S}chriften von {G}ottfried {W}ilhelm {L}eib niz}, year={1890}, address={Berlin}, tue={...} } @techreport{gert94, author="Gerth, editor., R. ", title={Verifying Sequentially Consistent Memory}, institution={TUE Computing Science Reports}, year={1994}, address={Eindhoven University of Technology}, number={44}, tue={IN BEZIT} } @misc{geuv90, author="Geuvers, J.H.", title="Type Systems for Higher Order Predicate Logic", year={1990}, month={May}, howpublished={Manuscript, Catholic University of Nijmegen}, tue={???} } @phdthesis{geuv93, author={Geuvers, J.H.}, title={Logics and Type Systems}, school={Catholic University of Nijmegen}, year={1993}, tue={IN BEZIT} } @article{geuvnede91, author="Geuvers, J.H. and Nederhof, M.J.", title={A modular proof of strong normalization for the {C}alculus of {C}onstructions}, journal={Journal of Functional Programming}, year={1991}, volume={1}, number={2}, pages={155--189}, tue={...} } @article{goed31, author={G\"odel, K.}, title={{\"U}ber formal unentscheidbare {S}\"atze der {P}rincipia {M}athematica und verwandter {S}ysteme {I}}, journal={Monatshefte f\"ur {M}athematik und {P}hysik}, volume={38}, year={1931}, pages={173--198}, note={German; English translation in \cite{heij67}, pages 592--618}, TUE={in heij67} } @incollection{goed44, author={G\"odel, K.}, title={Russell's mathematical logic}, booktitle={The Philosophy of B. Russell}, publisher={Evanston \&\ Chicago, Northwestern University}, year={1944}, editor={Schlipp, P.A.}, note={Also in \cite{benaputn83}}, tue={in wis cbd 83 phi} } @book{gordmelh93, editor={Gordon, M.J.C. and Melham, T.F.}, title={Introduction to HOL: A Theorem Proving Environment for Higher Order Logic}, publisher={Cambridge University Press}, year={1993}, address={London/New York} } @article{grue92, author={Grue, K.}, title={Map Theory}, journal={Theoretical Computer Science}, year={1992}, pages={1--133} } %HHHH @book{haeg94, author={Haegeman, L.}, title={Introduction to Government \& Binding Theory}, publisher={Blackwell}, address={Oxford}, year={1994}, edition={second}, tue={KUB LET E HAEG 1994} } @book{heij67, editor={van Heijenoort, J. }, title={From Frege to G\"odel: A Source Book in Mathematical Logic, 1879 --1931}, publisher={Harvard University Press}, address={Cambridge, Massachusetts}, year={1967}, tue={wis cbl 67 fre} } @phdthesis{hend93, author={Hendriks, H.}, title={Studied Flexibility: Categories and Types in Syntax and Semantic s}, school={Universiteit van Amsterdam}, year={1993}, tue={IN BEZIT} } @article{henk50, author={Henkin, L.}, year={1950}, volume={15}, journal={The Journal of Symbolic Logic}, title={Completeness in the Theory of Types}, pages={81--91}, tue={IN BEZIT} } @article{henk63, author={Henkin, L.}, year={1963}, pages={323--344}, volume={52}, journal={Fundamentae Mathematicae}, title={A Theory of Propositional Types}, tue={IN BEZIT} } @mastersthesis{heum92, author={van Heumen, R.}, title={Een intu\"{\i}tionistische verkenning van de constructie van {V} itali}, school={Department of Mathematics, Catholic University Nijmegen}, year={1992}, note={Dutch}, tue={IN BEZIT} } @book{heyt34, author={Heyting, A.}, title="Mathematische Grundlagenforschung. Intuitionismus. Beweistheorie ", publisher={Springer}, address={Berlin and New York}, series={Ergebnisse der Mathematik und ihrer Grenzgebiete}, year={1934}, tue={ipo cz 3} } @book{heyt56, author={Heyting, A.}, title={Intuitionism, an introduction}, year={1956}, address={Amsterdam}, series={Studies in Logic and the Foundations of Mathematics}, publisher={North Holland}, tue={...} } @book{heyt75, editor={Heyting, A.}, title={Brouwer: Collected Works}, publisher={North-Holland}, address={Amsterdam}, volume={1}, year={1975}, tue={wis cae 75 bro} } @article{hilb26, author={Hilbert, D.}, title={\"{U}ber das {U}nendliche}, journal={Mathematische Annalen}, volume={95}, year={1926}, note={Also in \cite{heij67}, pages 367--392}, tue={wis cbl 67 fro} } @inproceedings{hofm95, author={Hofmann, M.}, title={A simple model for quotient types}, booktitle={Typed lambda calculi and applications}, series={Lecture Notes in Computer Science}, publisher={Springer}, year={1977}, address={Berlin and New York}, pages={216--234}, } @unpublished{hube94, author={Hubey, H.M.}, title={On Hilbert's First Problem}, year={1994}, note={Montclair State College}, tue={IN BEZIT} } @phdthesis{hurk93, author={Hurkens, A.J.C.}, title={Borel determinacy without the axiom of choice}, school={Catholic University Nijmegen}, year={1993}, tue={IN BEZIT} } %IIII %JJJJ @phdthesis{jack95, author={Jackson, P.B.}, title={Enhancing the Nuprl Proff Development System and Applying it to Computational Abstract Algebra}, year={1962} } @unpublished{jack95a, author={Jackson, P.B.}, title={The {N}uprl Proof Development System, {V}ersion 4.1 Reference Manual and User's Guide}, year={1995}, note={Cornell University, Department of Computing Science, Ithaca, New York.}, tue={IN BEZIT} } @unpublished{jaco94, author={Jacobs, B.}, title={Quotients in Simple Type Theory}, note={Draft version of 30 March 1994}, tue={IN BEZIT} } @mastersthesis{jurj92, author={Jurjus, H.H.}, title={Groepen van permutaties van de natuurlijke getallen, mede in ver band met de theorie van berekenbare functies}, year={1992}, school={Vakgroep Wiskunde, Katholieke Universiteit Nijmegen}, note={Dutch}, tue={IN BEZIT} } %KKKK @article{kama92a, author={Kamareddine, F.}, title={$\lambda$-Terms, Logic, Determiners and Quantifiers}, year={1992}, journal={Journal of Logic, Language and Information}, volume={1}, pages={79--103}, tue={IN BEZIT} } @article{kama92b, author={Kamareddine, F.}, title={Set Theory and Nominalisation}, year={1992}, journal={Journal of Logic and Computation}, volume={2}, pages={579--604, 687--707}, tue={IN BEZIT} } @article{kama92c, author={Kamareddine, F.}, title={A system at the cross-roads of functional and logic programming} , year={1992}, journal={Science of Computer Programming}, volume={19}, pages={239--279}, tue={IN BEZIT} } @techreport{kama92d, author={Kamareddine, F.}, title={Are Types needed for Natural Language?}, year={1992}, number={20}, institution={TUE Computing Science Notes}, address={Eindhoven University of Technology}, tue={IN BEZIT} } @article{kamaklei93, author="Kamareddine, F. and Klein, E.", title={Nominalization, Predication and Type Containment}, year={1993}, journal={Journal of Logic, Language and Information}, volume={2}, pages={171--215}, tue={IN BEZIT} } @techreport{kamalaan95a, author="Kamareddine, F. and Laan, T.", title="A Reflection on {R}ussell's Ramified Types and {K}ripke's Hierar chy of Truths", year={1995}, institution={TUE Computing Science Notes}, number={18}, address={Eindhoven University of Technology}, tue={IN BEZIT}, } @techreport{kamalaan95b, author="Kamareddine, F. and Laan, T.", title="{K}ripke's Theory of Truth and {A}czel's {F}rege Structures", year={1995}, institution={TUE Computing Science Notes}, tue={IN BEZIT}, note={In preparation} } @article{kamalaan96, author="Kamareddine, F. and Laan, T.", title="A Reflection on {R}ussell's Ramified Types and {K}ripke's Hierar chy of Truths", year={1996}, journal="Journal of the Interest Group in Pure and Applied Logic", volume={4}, number={2}, pages={195--213}, tue={IN BEZIT}, note={{\tt http://www.mpi-sb.mpg.de:80/igpl/Bulletin/V4-2/Kamareddine.d vi.gz}} } @techreport{kamalaan96a, author="Kamareddine, F. and Laan, T.", title="A {C}orrespondence between {N}uprl and the {R}amified {T}heory o f {T}ypes", year={1996}, institution="TUE Computing Science Notes", tue={EIGEN WERK}, number="12", note="Also as Technical Report~TR-1996-18, Department of Computing Science, University of Glasgow, 1996" } @article{kamanede93, author="Kamareddine, F. and Nederpelt, R.", title={On stepwise explicit substitution}, journal={International Journal of Foundations of Computer Science}, volume={4}, pages={197--240}, year={1993}, tue={IN BEZIT} } @techreport{kamanede94, author="Kamareddine, F. and Nederpelt, R.P.", title={Canonical typing and {$\Pi$}-conversion}, year={1994}, number={2}, institution={TUE Computing Science Notes}, address={Eindhoven University of Technology}, tue={IN BEZIT} } @article{kamanede96, author="Kamareddine, F. and Nederpelt, R.P.", title={Canonical typing and {$\Pi$}-conversion in the {B}arendregt {C}u be}, year={1996}, volume={6}, number={2}, pages={245--267}, journal={Journal of Functional Programming}, tue={IN BEZIT} } @article{kamanede94b, author="Kamareddine, F. and Nederpelt, R.P.", title={A unified approach to type theory through a refined $\lambda$-ca lculus}, year={1994}, volume={136}, journal={Theoretical Computer Science}, pages={183--216}, tue={IN BEZIT} } @techreport{kanz91, author={Kanzawa, M.}, year={1991}, title={The Lambek Calculus enriched with additional connectives}, institution={ITLI Prepublications for Logic, Semantics and Philosophy o f Language}, tue={IN BEZIT reader categoriale grammatica} } @article{klee34, author={Kleene, S.C.}, title={Proof by cases in formal logic}, year={1934}, journal={Annals of Mathematics}, volume={35}, pages={529--544}, tue={IN BEZIT} } @article{klee35, author={Kleene, S.C.}, title={A theory of positive integers in formal logic}, year={1935}, journal={American Journal of Mathematics}, volume={57}, pages={153--173, 219--244}, tue={IN BEZIT} } @book{klee52, author={Kleene, S.C.}, title={Introduction to Metamathematics}, series={The University Series in Higher Mathematics}, year={1952}, publisher={D. Van Nostrand Comp.}, address={New York, Toronto}, tue={wis cbd 52 kle} } @article{klee81, author={Kleene, S.C.}, title={Origins of recursive function theory}, journal={Annals of the History of Computing}, year={1981}, volume={3}, number={1}, pages={52--67} } @article{kleeross35, author="Kleene, S.C. and Rosser, J.B.", title={The inconsistency of certain formal logics}, year={1935}, journal={Annals of Mathematics}, volume={36}, pages={630--636}, tue={IN BEZIT} } @incollection{klop92, author={Klop, J.W.}, title={Term Rewriting Systems}, booktitle={{\rm \cite{abragabbmaib92}}}, year={1992}, pages={1--116}, publisher={Oxford University Press}, tue={wis cbk 92 han} } @book{kneaknea62, author="Kneale, W. and Kneale, M.", title={The Development of Logic}, year={1962}, publisher={Oxford University Press}, tue={wm bft 62 kne} } @book{knee63, author={Kneebone, G.T.}, year={1963}, title={Mathematical Logic and the Foundations of Mathematics}, publisher={D. Van Nostrand Comp.}, address={London, New York, Toronto}, tue={exemplaar Nederpelt} } @phdthesis{koge95, author="Kogel, E. de", year={1995}, title={Equational Proofs in Tableaux and Logic Programming}, school={Tilburg University}, address={Tilburg}, tue={IN BEZIT} } @article{kolm32, author={Kolmogorov, A.N.}, title={Zur {D}eutung der {I}ntuitionistischen {L}ogik}, journal={Mathematisches Zeitschrift}, pages={58--65}, volume={35}, year={1932}, tue={...} } @article{krip75, author={Kripke, S.}, title={Outline of a Theory of Truth}, journal={Journal of Philosophy}, volume={72}, year={1975}, pages={690--716}, tue={---} } @article{kupe93, author={Kuper, J.}, title={An axiomatic theory for partial functions}, journal={Information and Computation}, year={1993}, pages={104-150} } @phdthesis{kupe94, title={Partiality in Logic and Computation}, author={Kuper, J.}, year={1994}, school={University of Twente}, address={Enschede}, tue={IN BEZIT} } %LLLL @mastersthesis{laan93, author={Laan, T.}, title={Spelen met Oneindig in de intu\"{\i}tionistische wiskunde}, school={Department of Mathematics, Catholic University Nijmegen}, year={1993}, note={Dutch}, tue={IN BEZIT} } @techreport{laan94, author={Laan, T.}, year={1994}, number={33}, title={A Formalization of the {R}amified {T}ype {T}heory}, institution={TUE Computing Science Reports}, address={Eindhoven University of Technology}, tue={EIGEN WERK} } @inproceedings{laan95a, author={Laan, T.}, title={{A} {M}odern {V}iew on the {R}amified {T}heory of {T}ypes}, booktitle={{P}roceedings {C}{S}{N} 95}, editor={van Vliet, J.C.}, year={1995}, publisher={{S}tichting {M}athematisch {C}entrum}, address={Amsterdam}, pages={122--133}, tue={EIGEN WERK} } @techreport{laan96a, author={Laan, T.}, year={1996}, title={{\sc Automath} and {P}ure {T}ype {S}ystems}, institution={TUE Computing Science Reports}, address={Eindhoven University of Technology}, number="11", tue={EIGEN WERK} } @article{laannede96, author={Laan, T. and Nederpelt, R.P.}, year={1996}, title={{A} Modern Elaboration of the {R}amified {T}heory of {T}ypes}, journal={Studia Logica}, volume={57}, number={3}, tue={EIGEN WERK} } @article{lamb58, author={Lambek, J}, year={1958}, title={The mathematics of sentence structure}, journal={American Mathematical Monthly}, volume={65}, pages={154--170}, note={Also in \cite{buszmarcbent88}}, tue={in XF 88 (IPO), 153-172}, } @article{lambscot81, author="Lambek, J. and Scott, P.J.", year={1981}, title={Intuitionist type theory and foundations}, journal={Journal of Philosophical Logic}, volume={10}, pages={101--115}, tue={IN BEZIT} } @mastersthesis{leuw95, author={Leuw, B.-J. de}, title={Generalisations in the lambda calculus and its type theory}, year={1995}, school={Department of Computing Science, Catholic University of Nijmegen}, tue={IN BEZIT} } @book{lloy93, author={Lloyd, J.W.}, year={1993}, title={Foundations of Logic Programming}, edition={second}, publisher={Springer}, address={Berlin and New York}, series={Symbolic Computation -- Artificial Intelligence}, tue={IN BEZIT} } @techreport{long86, author={Longo, G.}, title={On {C}hurch's Formal Theory of Functions and Functionals}, year={1987}, number={9}, institution={Department of Computing Science, Pisa University}, tue={Exemplaar Nederpelt} } @misc{luo, author={Luo, Z.}, title={{E}{C}{C} and extended {C}alculus of {C}onstructions}, howpublished={Department of Computer Science, University of Edinburgh}, tue={...} } @misc{luo_94, author={Luo, Z.}, title={On the totality of propositions in type theory}, year={1994}, howpublished={Submitted for TLCA '95}, tue={IN BEZIT} } %MMMM @incollection{mati71, author={Matijasevi{\v{c}}, Yu.V.}, title={On recursive unsolvability of Hilbert's tenth problem}, booktitle={Fourth International Congress for Logic, methodology and philosophy of science}, year={1971}, publisher={North-Holland}, address={Amsterdam}, note={Studies in Logic and the Foundations of Mathematics {\bf 74}}, pages={89--110} } @inproceedings{mart75, author={Martin-L\"of, P.}, title={An intuitionistic theory of types: predicative part}, booktitle={Logic Colloquium '73}, editor="Rose, H.E. and Shepherdson, J.C.", year={1975}, publisher={North-Holland}, address={Amsterdam}, pages={73--118}, note={Studies in Logic and the Foundations of Mathematics {\bf 80}}, tue={wis cbl 71 log} } @inproceedings{mart82, author={Martin-L\"of, P.}, title={Constructive mathematics and computer programming}, booktitle={Sixth International Congress for Logic, Methodology and Philosophy of Science}, year={1982}, publisher={North-Holland}, address={Amsterdam}, pages={153--175}, tue={???} } @techreport{mauwmeul95, author="Mauw, S. and van der Meulen, E.A.", title="Specification of tools for {M}essage {S}equence {C}harts", year={1995}, number={17}, institution={TUE Computing Science Reports}, address={Eindhoven University of Technology}, tue={IN BEZIT} } @techreport{mauwreni94, author="Mauw, S. and Reniers, M.A.", title={An Algebraic Semantics of Basic Message Sequence Charts}, year={1994}, number={17}, institution={TUE Computing Science Notes}, address={Eindhoven University of Technology}, tue={IN BEZIT} } @techreport{mauwreni95, author="Mauw, S. and Reniers, M.A.", title={Empty Interworkings and Refinement Semantics of Interworkings Re vised}, year={1995}, number={12}, institution={TUE Computing Science Reports}, address={Eindhoven University of Technology}, tue={IN BEZIT} } @techreport{mauwmuld94, author="Mauw, S. and Mulder, H.", title={Regularity of {B}{P}{A}-Systems is Decidable}, year={1994}, number={27}, institution={TUE Computing Science Notes}, address={Eindhoven University of Technology}, tue={IN BEZIT} } @book{mcca67, editor={McCall, S.}, title={Polish Logic 1920--1939}, year={1967}, publisher={Oxford University Press}, address={London}, tue={Koninklijke Bibliotheek 7028 C 14} } @article{melh93, author={Melham, T.F.}, title={The {H}{O}{L} Logic Extended with Quantification over Type Varia bles}, year={1993}, pages={7--24}, journal={Formal Methods in System Designs}, tue={IN BEZIT} } @Book{milntoftharp90, author= "Robin Milner and Mads Tofte and Robert Harper", title= "The Definition of {S}tandard {ML}", publisher= "The MIT Press", year= 1990 } @Article{moggi91, author= "Eugenio Moggi", title= "Notions of Computation and Monads", journal= "Information and Computation", year= 1991, volume= 93, pages= "55-92" } @incollection{mont73, author={Montague, R.}, editor="Hintikka, J. and Moravcsik, J.M.E. and Suppes, P.", booktitle="Approaches to Natural Language", title="The proper treatment of quantification in ordinary {E}nglish", year={1973}, publisher={Dordrecht}, tue={---} } @phdthesis{moor88, author={Moortgat, M.}, year={1988}, school={University of Utrecht}, title={Categorial Investigations: Logical and Linbuistical Aspects of t he Lambek Calculus}, tue={cm apy 88 moo} } @misc{mooroehr93, author="Moortgat, M. and Oehrle, D.", title={Lecture Notes on Categorial Grammar}, howpublished={Fifth European Summer School in Language, Logic and Infor mation, Lisbon}, year={1993}, month={aug}, tue={IN BEZIT reader categoriale grammatica} } @misc{morr??, author={Morrill, G.}, title={Discontinuity and Pied-Piping in Categorial Grammar}, tue={IN BEZIT, reader categoriale grammatica} } @techreport{morr92, author={Morrill, G.}, title={Type-Logical Grammar}, year={1992}, number={2}, month={jan}, institution={OTS Working Papers}, tue={IN BEZIT} } %NNNN @inproceedings{nadamill88, author = {G. Nadathur and D. Miller}, title = {An Overview of {$\lambda$Prolog}}, booktitle = {Logic Programming: Proceedings of the Fifth International Conference and Symposium, Volume 1}, publisher = {MIT Press}, month = {August}, year = {1988}, editor = {Robert A. Kowalski and Kenneth A. Bowen}, address = {Cambridge, Massachusetts}, pages = {810--827}, source = {ergobib} } @book{nede87, author="Nederpelt, R.P.", title="De taal van de wiskunde", year="1987", publisher="Versluys", address="Almere", tue="wis cbk 87 ned" } @article{nedekama92, author="Nederpelt, R.P. and Kamareddine, F.", title="A useful lambda notation", journal="The Journal of Symbolic Logic", year={1992}, note="Paper presented at the 1992 Logic Colloquium, Vesprem, Hungary", } @article{neum25, author={von Neumann, J.}, title={Eine Axiomatisierung der Mengenlehre}, journal={J. reine angew. Math.}, year={1925}, volume={154}, pages={219--240} } @mastersthesis{nies93, author={Niesten, S.}, year={1993}, title={Minstens \&\ {H}oogstens}, school={Department of Mathematics, Catholic University Nijmegen}, note={Dutch}, tue={IN BEZIT} } @proceedings{nieu95, editor={Nieuwendijk, A.}, title={Accolade '94}, year={1995}, organization={Dutch Graduate School in Logic}, tue={IN BEZIT} } %OOOO @book{odon77, author={O'Donnell, M.J.}, title={Computing in Systems Described by Equations}, volume={58}, series={Lecture Notes in Computer Science}, publisher={Springer}, address={Berlin and New York}, year={1977}, tue={---} } %PPPP @article{pars71, author={Parsons, C.}, title={The iterative conception of Set}, journal={The Journal of Philosophy}, volume={68}, year={1971}, pages={215--237}, tue={IN BEZIT} } @incollection{pars79, author={Parsons, T.}, year={1979}, title="The theory of types and ordinary language", booktitle="Linguistics, Philosophy and Montague Grammar", editor={Davies, S. and Mithun, M.}, publisher="University of Texas Press", address={Austin}, tue={---} } @book{pean89, author={Peano, G.}, year={1889}, title={Arithmetices principia, nova methodo exposita}, publisher={Bocca}, address={Turin}, note={English translation in \cite{heij67}, pages 83--97} } @techreport{pelehuizpete94, author="Peleska, J. and Huizing, C. and Petersohn, C.", title={A Comparison of {W}ard \&\ {M}ellor's Transformation Schema with State- \&\ Activitycharts}, year={1994}, number={11}, institution={TUE Computing Science Notes}, address={Eindhoven University of Technology}, tue={IN BEZIT} } @techreport{pent92, author={Pentus, M.}, title={Lambek grammars are context free}, year={1992}, institution={Department of Mathematical Logic, Faculty of Mechanics and Mathematics, Moscow University}, tue={IN BEZIT reader categoriale grammatica} } @techreport{pere94, author={Peremans, W.}, title={Ups and Downs of Type Theory}, institution={TUE Computing Science Notes}, year={1994}, number={14}, address={Eindhoven University of Technology}, tue={IN BEZIT} } @mastersthesis{pete92, author={Peters, R.H.M.T.}, title={Oorsprong van de Typentheorie}, year={1992}, school={Eindhoven University of Technology}, note={Dutch}, tue={IN BEZIT} } @book{poin16, author={Poincar\'e, H.}, title={Science et m\'ethode}, publisher={Flammarion}, address={Paris}, year={1916} } @book{poin02, author={Poincar\'e, H.}, title={La Science et l'Hypoth\`ese}, publisher={Flammarion}, address={Paris}, year={1902} } @phdthesis{poll94, author={Poll, E.}, title={A Programming Logic Based on Type Theory}, school={Eindhoven University of Technology}, year={1994}, tue={IN BEZIT} } %QQQQ @article{quin37, author={Quine, W.~Van Orman}, title={New Foundations for Mathematical Logic}, year={1937}, journal={American Mathematical Monthly}, volume={44}, note={Also in \cite{quin61a}}, tue={wm bft 61 van} } @book{quin52, author={Quine, W.~Van Orman}, title={Methods of Logic}, year={1952}, publisher={Routledge \&\ Kegan Paul}, address={London}, tue={wm bft 58 orm} } @article{quin61, author={Quine, W.~Van Orman}, title={Paradox}, journal={Scientific American}, volume={206}, year={1962}, note={Also in \cite{quin66}}, tue={quin66, wm bec 66 qui} } @book{quin61a, author={Quine, W.~Van Orman}, title={From a Logical Point of View: 9 Logico-Philosophical Essays}, publisher={Harvard University Press}, address={Cambridge, Massachusetts}, year={1961}, tue={wm bft 61 van} } @book{quin63, author={Quine, W.~Van Orman}, title={Set Theory and its Logic}, publisher={Harvard University Press}, address={Cambridge, Massachusetts}, year={1963}, tue={wm cbk 63 qui} } @book{quin66, author={Quine, W.~Van Orman}, title={The Ways of Paradox and other essays}, publisher={Random House}, address={New York}, year={1966}, tue={wm bec 66 qui} } %RRRR @techreport{raamseve95, author="van Raamsdonk, F. and Severi, P.", title="On Normalisation", year={1995}, number={20}, institution={Computing Science Notes}, address={Eindhoven University of Technology}, tue={IN BEZIT} } @book{brai50, title={F.~P. Ramsay: The foundations of mathematics and other logical essays}, editor={Braithwaite, R.B.}, year=1960, publisher={Routledge \& Kegan Paul}, address={London} } @unpublished{rave94, author={Raven, D.}, year={1994}, title={The Enculturation of Logical Practice}, note={Essay}, tue={IN BEZIT via logicagroep Sarlemijn/Kroes} } @InProceedings{reyn74, author= "J.C. Reynolds", title= "On the Relation between Direct and Continuation Semantics", booktitle= "2nd Colloquium on Automata, Languages and Programming", year= 1974, editor= "Jacques Loeckx", series={Lecture Notes in Computer Science}, number=14, pages= "141-156", OPTpublisher=S-V, address= "Saarbr{\"{u}}cken, West Germany", month= Jul } @book{riemwill86, author="van Riemsdijk, H. and Williams, E.", year={1986}, title={Introduction to the Theory of Grammar}, publisher={Massachusetts Institute of Technology Press}, address={Cambridge, Massachusetts}, series={Current Studies in Linguistics {\bf 12}}, tue={KUB LET e4 RIEM 1986} } @article{robi37, author={Robinson, R.M.}, title={The Theory of Classes---A Modification of Von Neumann's System}, year={1937}, journal={J. Symbolic Logic}, volume={2}, pages={29--36} } @phdthesis{rooi63, author={van Rooij, A.C.M.}, title={On lattices of rings of sets}, school={Utrecht University}, year={1963}, tue={IN BEZIT} } @phdthesis{roor91, author={Roorda, D.}, title={Resource Logics: Proof-theoretical investigations}, school={University of Amsterdam}, year={1991}, tue={IN BEZIT reader categoriale grammatica} } @proceedings{rootstaa68, editor="van Rootselaar, B. and Staal, J.F.", year={1968}, title={Logic, Methodology and Philosophy of Science III}, publisher={North-Holland, Amsterdam}, address={Amsterdam}, organization={Studies in Logic and the Foundations of Mathematics}, tue={wis cbd 62 log} } @article{ross35, author={Rosser, J.B.}, title={A mathematical logic without variables}, journal={Annals of Mathematics}, volume={36}, year={1935}, pages={127--150}, tue={IN BEZIT} }@inproceedings{ross82, author = {J.B. Rosser}, title = {Highlights of the history of lambda-calculus}, booktitle = {ACM Symposium on Lisp and Functional Programming}, year = {1982}, month = {August}, publisher = {ACM Press}, address = {Pennysylvania}, pages = {216-225} } @misc{russ02, author={Russell, B.}, title={Letter to {F}rege}, year={1902}, howpublished={English translation in \cite{heij67}, pages 124--125}, tue={wis cbl 67 fro} } @book{russ03, author={Russell, B.}, title={The Principles of Mathematics}, year={1903}, publisher={Allen \&\ Unwin}, address={London}, tue={wis cbb 72 rus} } @article{russ08, author={Russell, B.}, title={Mathematical logic as based on the theory of types}, journal={American Journal of Mathematics}, volume={30}, year={1908}, note={Also in \cite{heij67}, pages 150--182}, tue={wis cbl 67 fro} } @book{russ19, author={Russell, B.}, title={Introduction to Mathematical Philosophy}, year={1919}, publisher={Allen \&\ Unwin}, address={London}, tue={centr mag cbd 60 rus} } %SSSS @article{sanc64, author={Sanchis, L.E.}, title={Types in Combinatory Logic}, volume={5}, journal={Notre Dame Journal of Formal Logic}, pages={161--180}, year={1964}, tue={IN BEZIT} } @article{schu60, author={Sch\"utte, K.}, year={1960}, journal={The Journal of Symbolic Logic}, volume={25}, title={Syntactical and Semantical Properties of Simple Type Theory}, pages={305--326}, tue={IN BEZIT} } @article{schw76, author={Schwichtenberg, H.}, year={1976}, title={Definierbare Funktionen im $\l$-Kalk\"ul mit Typen}, journal={Archief f\"ur Mathematische Logik}, volume={25}, pages={113-114} } @article{scho24, author={Sch\"onfinkel, M.}, year={1924}, title={\"{U}ber die {B}austeine der mathematischen {L}ogik}, journal={Mathematische Annalen}, volume={92}, note={Also in \cite{heij67}, pages 355--366}, tue={wis cbl 67 fro} } @book{sell87, author={Sells, P.}, year={1987}, title={Lectures on contemporary syntactic theories}, publisher={Center for the Study of Language and Information}, address={Stanford}, series={CSLI Lecture Notes {\bf 3}}, tue={KUB: LET E4 SELL 1985} } @misc{smitgerrmaaslaan93, author="Smit, J. and Gerritse, G. and Maassen, H. and Laan, T.", title={Kansrekening}, year={1993}, howpublished={Lecture notes, Catholic University Nijmegen}, note={Dutch}, tue={IN BEZIT} } @phdthesis{spri95, author="Springintveld, J.", title="Algorithms for Type Theory", school="Department of Philosophy, Utrecht University", year="1995", tue={IN BEZIT} } @book{swar89, author={Swart, H.C.M. de}, year={1989}, title={Filosofie van de Wiskunde}, publisher={Martinus Nijhoff}, address={Leiden}, series={Serie Wetenschapsfilosofie}, note={Dutch}, tue={wm cbd 89 swa} } @proceedings{shya93, TITLE = {Foundations of software technology and theoretical computer science}, NOTE = {Proceedings of the conference held in Bombay, December 15--17, 1993}, EDITOR = {Shyamasundar, R. K.}, PUBLISHER = {Springer-Verlag}, ADDRESS = {Berlin}, YEAR = {1993}, PAGES = {xiv+455}, ISBN = {3-540-57529-4}, } %TTTT @article{tait67, author={Tait, W.W.}, year={1967}, volume={32}, journal={The Journal of Symbolic Logic}, pages={198--212}, title={Intensional Interpretations of Functionals of Finite Type I}, tue={IN BEZIT} } @article{take53, author={Takeuti, G.}, year={1953}, title={On a generalized logic calculus}, journal={Japanese Journal of Mathematics}, volume={23}, pages={39--96}, tue={IN BEZIT} } @article{tars36, author={Tarski, A.}, title={Der {W}ahrheitsbegriff in den formalisierten {S}prachen}, journal={Studia Philosophica}, volume={1}, year={1936}, pages={261--405}, note={German translation by L. Blauwstein from the Polish original (193 3) with a postscript added}, tue={} } @techreport{terl89, author="Terlouw, J.", title={Een nadere bewijstheoretische analyse van {G}{S}{T}{T}'s}, institution={Department of Computer Science}, address={University of Nijmegen}, year={1989}, tue={...} } %UUUU %VVVV @phdthesis{veld81, author={Veldman, W.H.M.}, title={Investigations in Intuitionistic Hierarchy Theory}, year={1981}, school={Catholic University Nijmegen}, tue={IN BEZIT} } @misc{veld84, author={Veldman, W.H.M.}, title={Modellentheorie}, year={1984}, howpublished={Lecture notes, Catholic University Nijmegen}, note={Dutch}, tue={IN BEZIT} } @misc{veld87, author={Veldman, W.H.M.}, year={1987}, title={Berekenbaar en Bewijsbaar (Recursietheorie)}, howpublished={Lecture Notes, Catholic University Nijmegen}, note={Dutch}, tue={IN BEZIT} } @misc{veld91, author={Veldman, W.H.M.}, year={1991}, title={Intu\"{\i}tionistische Wiskunde}, howpublished={Lecture Notes, Catholic University Nijmegen}, note={Dutch}, tue={IN BEZIT} } @techreport{vene93, author={Venema, Y.}, title={Meeting strength in substructural logics}, institution={OTS Working Papers}, year={1993}, tue={IN BEZIT reader categoriale grammatica} } @mastersthesis{vere93, author={Vereijken, J.J.}, title={Graph Grammars and Operations on Graphs}, year={1993}, school={Department of Computer Science, Leiden University}, tue={IN BEZIT} } @techreport{verh93, author={Verhoef, C.}, title={A general conservative extension theorem in process algebra}, institution={TUE Computing Science Notes}, address={Eindhoven University of Technology}, year={1993}, number={38}, tue={IN BEZIT} } @article{vrij85, author={Vrijer, R.~{de} }, journal={The Journal of Symbolic Logic}, title={A direct Proof of the Finite Developments Theorem}, volume={50}, pages={339--343}, number={2}, year={1985} } %WWWW @unpublished{wall93, author={Wallgren, J.}, title={Types in Logic Programming}, note={Draft version of end 1993}, tue={IN BEZIT} } @book{warn83, author={Warner, F.W.}, title={Foundations of differentiable manifolds and Lie groups}, year=1983, publisher={Springer}, address={Berlin and New York}, series={Gra\-duate Texts in Mathematics, 94} } @book{weyl18, author={Weyl, H.}, title={Das Kontinuum}, year={1918}, publisher={Veit}, address={Leipzig}, note={German; also in: Das Kontinuum und andere Monographien, Chelsea P ub.Comp., New York, 1960}, tue={wis cad 60 kon} } @article{weyl46, author={Weyl, H.}, title={Mathematics and Logic: A brief survey serving as preface to a re view of ``{T}he {P}hilosophy of {B}ertrand {R}ussell''}, journal={American Mathematical Monthly}, year={1946}, tue={IN BEZIT} } @book{wild65, author="Wilder, R.L.", title="The Foundations of Mathematics", edition={second}, year={1965}, publisher={Robert E.~Krieger Publishing Company, Inc.}, address={New York}, tue={wis CBB 80 WIL} } @book{whit10, author="Whitehead, A.N. and Russell, B.", year={$1910^1$, $1927^2$}, title={Principia Mathematica Vol 1 and 2}, publisher={Cambridge University Press}, tue={wis cbb 63 whi} } %XXXX %YYYY %ZZZZ %\input{extrawil.bib} @article{buch92, author={B. Buchberger}, title={Gr{\"o}bner Bases: An Introduction}, journal={Lecture Notes in Computer Science}, volume={623}, pages={378--379}, year={1992}, publisher={Springer}, address={Berlin and New York} } @inproceedings{buch85, author={B. Buchberger}, title={Gr{\"o}bner Bases: An Algorithmic Method in Polynomial Ideal Theory}, booktitle={Multidimensional Systems Theory}, editor={N.K. Bose}, pages={184-232}, year={1985}, publisher={Reidel}, address={Dordrecht} } @article{chur3233, author={Church, A.}, title={A set of postulates for the foundation of logic}, journal={Ann. of Math.}, volume={33}, pages={346--366}, year={1932}, note={Second paper with same title in Vol. 33, pages 839--864, of same journal} } @misc{stat76, author={Statman, R.}, title={Personal communication}, year={1976} } @incollection{klee74, author={Kleene, S.C.}, title={Reminiscences of logicians}, year={1975}, editor={Crossley, J.N.}, booktitle={Algebra and logic (Fourteenth Summer Res. Inst., Austral. Math. Soc., Monash Univ., Clayton, 1974)}, pages={1--62}, publisher={Springer}, address={Berlin and New York}, series={Lecture Notes in Mathematics}, volume={450} } @article{turi37, author={Turing, A.M.}, title={Computability and lambda definability}, journal={J. Symbolic Logic}, volume={2}, year={1937}, pages={153--163} } @article{turi36, author={A.M. Turing}, title={On Computable Numbers with an Application to the {E}ntscheidungsproblem}, journal={Proc. London Math. Soc. (2)}, volume={42}, year={1936}, pages={230--265}, annote={Hodges page 96 note 2.37; Reprinted in {\em The Undecidab le}.} } @article{skol23, author={Skolem, T.}, title={Begr{\"u}ndung der elementaren {A}rithmetik durch die rekurrierende {D}enkweise ohne {A}nwendung scheinbarer {V}er{\"e}nderlichen mit unendlichem {A}usdehnungsbereich}, journal={Videnskapsselskapets skrifter, I. Matematisk-naturvidenskabelig klasse}, volume={6}, year={1923}, note={English translation in \citeasnoun{heij67}, pp 302--333} } @book{vanHeijenoortJ:frofgs, author = {van Heijenoort, Jan}, title = {From {F}rege to {G}{\"o}del: a Source Book in Mathematical Logic, 1879--1931}, publisher = {Harvard University Press}, address = {Cambridge, MA}, libcongress = {67-10905}, isbn = {0 674 32450 1}, year = {1967}, reprinted = {1971, 1976}, pages = {xi+665} } @incollection{gandturi80, author={Gandy, R.O.}, title={An early proof of normalization by {A.M. Turing}}, booktitle={To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism}, editors={Seldin, J.P. and J.R. Hindley}, publisher={Academic Press}, year={1980}, pages={453--455} } @article{davi82, title={Why {G{\"o}del} Didn't Have {Church's} Thesis}, author={M. Davis}, pages={3--24}, journal={Information and Control}, month={jul / aug}, year={1982}, volume={54}, number={1/2} } @inproceedings{krei68, author={Kreisel, G.}, title={Church's thesis: A kind of reducibility axiom for constructive mathematics}, booktitle={Intuitionism and Proof Theory, Proc. Conf., Buffalo, N.Y., 1968}, pages={121--150}, publisher={North-Holland} } @inproceedings{debr68, author={de Bruijn, N.G.}, title={The Mathematical Language {AUTOMATH}, Its Usage, and Some of Its Extensions}, editor={M. Laudet}, pages={29--61}, booktitle={Proceedings of the Symposium on Automatic Demonstratio n}, year={1968}, publisher={Springer}, series={Lecture Notes in Mathematics}, volume={125}, address={Berlin and New York}, month={dec}, keywords={Automath} } @incollection{bohm63, author={{B\"{o}hm}, C.}, title={The CUCH as a Formal and Description Language}, booktitle={Annual Review in Automatic Programming, Vol. 3}, editor={Richard Goodman}, publisher={Pergamon Press}, address={Oxford}, year={1963}, pages={179--197}, checked={11 March 1993} } @article{barebare97, author={Barendregt, H.~P. and Barendsen, E.}, title={Efficient computations in formal proofs}, year=1997, note={to appear} } @proceedings{barenipk94, editor = {H.P. Barendregt and Tobias Nipkow}, booktitle = {Types for proofs and programs: international workshop {TYPES} '93, Nijmegen, The Netherlands, May 24--28, 1993: selected papers}, title = {Types for proofs and programs: international workshop {TYPES} '93, Nijmegen, The Netherlands, May 24--28, 1993: selected papers}, volume = {806}, publisher = {Spring{\-}er-Ver{\-}lag}, address = {Berlin, Germany~/ Heidelberg, Germany~/ London, UK~/ etc.}, pages = {383}, year = {1994} } @Article{bareghil99, author = "Barendregt, Henk and Ghilezan, Sylvia", title = "Lambda terms for natural deduction, sequent calculus and cut-elimination", OPTcrossref = "", OPTkey = "", journal = "Journal of Functional Porgramming", OPTyear = "", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", note = "To appear.", OPTannote = "" } @InProceedings{reyn74, author="J.C. Reynolds", title="On the Relation between Direct and Continuation Semantics" , booktitle="2nd Colloquium on Automata, Languages and Programming", year=1974, editor="Jacques Loeckx", series=LNCS, number=14, pages="141-156", OPTpublisher=S-V, address="Saarbr{\"{u}}cken, West Germany", month=Jul } @Book{milntoftharp90, author="Robin Milner and Mads Tofte and Robert Harper", title="The Definition of {S}tandard {ML}", publisher="The MIT Press", year=1990 } @Article{mogg91, author="Eugenio Moggi", title="Notions of Computation and Monads", journal="Information and Computation", year=1991, volume=93, pages="55-92" } @article{land65, author={P.J. Landin}, title={A correspondence between {ALGOL} 60 and {Church}'s lambda notation}, year={1965}, journal={Communications of the ACM}, volume={8}, pages={89--101,158--165} } @incollection{scot80a, author={D.S. Scott}, title={Relating Theories of the {$\lambda$}-Calculus}, checked={Yes}, pages={403--450}, crossref={PierceBC,CurryFestschrift} } @book{leeu90, booktitle = {Handbook of Theoretical Computer Science}, editor = {J. van Leeuwen}, publisher = {North-Holland, MIT-Press}, title = {Handbook of Theoretical Computer Science}, year = {1990}, volume={A, B}, } @incollection{scot80, author={D.S. Scott}, title={Lambda Calculus: Some Models, Some Philosophy}, booktitle={The Kleene Symposium}, editor={J. Barwise and H.J. Keisler and K. Kunen}, publisher={North-Holland Publishing Company}, year={1980}, pages={223--265} } @article {scot75a, AUTHOR = {Scott, Dana}, TITLE = {Some philosophical issues concerning theories of combinators}, BOOKTITLE = {$\lambda $-calculus and computer science theory (Proc. Sympos., Rome, 1975)}, PAGES = {346--366. Lecture Notes in Comput. Sci., Vol. 37}, PUBLISHER = {Springer}, ADDRESS = {Berlin}, YEAR = {1975}, MRCLASS = {02C20}, MRNUMBER = {57 #15986}, MRREVR = {B. Lercher}, } @incollection{scot75, OPTcrossref = "", OPTkey = "", author = "Scott, D.S.", title = "Open problem", booktitle = "Lambda Calculus and Computer Science Theory", year = "1975", publisher={Springer}, address={Berlin}, series={Lecture Notes in Computer Science}, volume={37}, pages= "369", OPTmonth = "", OPTnote = "", OPTannote = "" } @incollection{scot70, author={Scott, D.S.}, booktitle={Symposium on Automated Demonstration}, editor={M. Laudet, D. Lacombe and M. Schuetzenberger}, publisher={Springer}, address={Berlin}, series={Lecture Notes in Mathematics}, volume={125}, title={Constructive Validity}, year={1970}, pages={237--275}} } @book{gierhofm80, author={Gierz, G.K. and Hofmann, Karl Heinrich and Keimel, Klaus and Lawson Jimmie D. and Mislove, M.W. and Scott, D.S.}, title={A Compendium of Continuous Lattices}, publisher={Springer}, address={Berlin and New York}, year={1980}, } @book{Pey87, author = {S.L. {Peyton~Jones}}, title = {The Implementation of Functional Programming Languages}, publisher = {Prentice-Hall}, year = {1987} } @article{huda94b, author={P. Hudak and S. Peyton Jones and P. Walder and B. Boutel and J. Fairbairn and J. Fasel and M.M. Guzman and K. Hammond and J. Hughes and T. Johnsson and D. Kieburtz and R. Nikhil and W. Partain and J. Peterson}, title={Report on the programming language {Haskell}: a non-strict, purely functional language (Version 1.2)}, journal={ACM SIG{\-}PLAN Notices}, volume={27}, number={5}, pages={Ri--Rx, R1--R163}, month={may}, year={1992}, coden={SINODQ}, issn={0362-1340}, bibdate={Sat Dec 16 15:47:40 1995} } @proceedings{szab69, title={The {C}ollected {P}apers of {G}erhard {G}entzen}, editor={Szabo, M.E.}, publisher={North-Holland}, address={Amsterdam}, note={Studies in Logic and the Foundations of Mathematics}, year={1969} } @Article{Reynolds:LaSC93, author = "J.C. Reynolds", title = "The Discoveries of Continuations", pages = "233-247", journal = "LISP and Symbolic Computation", year = 1993, volume = 6, number = "3/4", month = Dec } @TechReport{Steele:78, author = "Guy L. {Steele Jr.}", title = "RABBIT: A Compiler for {S}CHEME", institution = "Artificial Intelligence Laboratory, Massachusetts Institute of Technology", year = 1978, number = "AI-TR-474", address = "Cambridge, Massachusetts", month = May } @article {coppdezavenn81, AUTHOR = {Coppo, M. and Dezani-Ciancaglini, M. and Venneri, B.}, TITLE = {Functional characters of solvable terms}, JOURNAL = {Z. Math. Logik Grundlag. Math.}, FJOURNAL = {Zeitschrift f\"ur Mathematische Logik und Grundlagen der Mathematik}, VOLUME = {27}, YEAR = {1981}, NUMBER = {1}, PAGES = {45--58}, ISSN = {0044-3050}, CODEN = {ZMLGAQ}, } @article {barecoppdeza83, AUTHOR = {Barendregt, Henk and Coppo, Mario and Dezani-Ciancaglini, Mariangiola}, TITLE = {A filter lambda model and the completeness of type assignment}, JOURNAL = {J. Symbolic Logic}, FJOURNAL = {The Journal of Symbolic Logic}, VOLUME = {48}, YEAR = {1983}, NUMBER = {4}, PAGES = {931--940 (1984)}, ISSN = {0022-4812}, CODEN = {JSYLA6}, } @article {coppcian95, AUTHOR = {Coppo, Mario and Giannini, Paola}, TITLE = {Principal types and unification for simple intersection type systems}, JOURNAL = {Inform. and Comput.}, FJOURNAL = {Information and Computation}, VOLUME = {122}, YEAR = {1995}, NUMBER = {1}, PAGES = {70--96}, ISSN = {0890-5401}, }@article {coppferr93, AUTHOR = {Coppo, Mario and Ferrari, Alberto}, TITLE = {Type inference, abstract interpretation and strictness analysis}, NOTE = {A collection of contributions in honour of Corrado B\"ohm on the occasion of his 70th birthday}, JOURNAL = {Theoret. Comput. Sci.}, FJOURNAL = {Theoretical Computer Science}, VOLUME = {121}, YEAR = {1993}, NUMBER = {1-2}, PAGES = {113--143}, ISSN = {0304-3975}, CODEN = {TCSDI}, } @article {coppdezazacc87, AUTHOR = {Coppo, M. and Dezani-Ciancaglini, M. and Zacchi, M.}, TITLE = {Type theories, normal forms, and ${D}\sb \infty$-lambda-models}, JOURNAL = {Inform. and Comput.}, FJOURNAL = {Information and Computation}, VOLUME = {72}, YEAR = {1987}, NUMBER = {2}, PAGES = {85--116}, ISSN = {0890-5401}, } @incollection {coppdezahonslong84, AUTHOR = {Coppo, M. and Honsell, F. and Dezani-Ciancaglini, M. and Longo, G.}, TITLE = {Extended type structures and filter lambda models}, BOOKTITLE = {Logic colloquium '82 (Florence, 1982)}, PAGES = {241--262}, PUBLISHER = {North-Holland}, ADDRESS = {Amsterdam}, YEAR = {1984}, } @incollection {coppdezalong83, AUTHOR = {Coppo, M. and Dezani, M. and Longo, G.}, TITLE = {Applicative information systems}, BOOKTITLE = {CAAP '83 (L'Aquila, 1983)}, PAGES = {35--64}, PUBLISHER = {Springer}, ADDRESS = {Berlin}, YEAR = {1983}, } @article {coppdeza80, AUTHOR = {Coppo, M. and Dezani-Ciancaglini, M.}, TITLE = {An extension of the basic functionality theory for the $\lambda $-calculus}, JOURNAL = {Notre Dame J. Formal Logic}, FJOURNAL = {Notre Dame Journal of Formal Logic}, VOLUME = {21}, YEAR = {1980}, NUMBER = {4}, PAGES = {685--693}, ISSN = {0029-4527}, CODEN = {NDJFAM}, } @incollection {coppdezavenn80, AUTHOR = {Coppo, M. and Dezani-Ciancaglini, M. and Venneri, B.}, TITLE = {Principal type schemes and $\lambda $-calculus semantics}, BOOKTITLE = {To H. B. Curry: essays on combinatory logic, lambda calculus and formalism}, PAGES = {535--560}, PUBLISHER = {Academic Press}, ADDRESS = {London}, YEAR = {1980}, } @article {honsleni99, AUTHOR = {Honsell, Furio and Lenisa, Marina}, TITLE = {Semantical analysis of perpetual strategies in $\lambda$-calculus}, NOTE = {Gentzen (Rome, 1996)}, JOURNAL = {Theoret. Comput. Sci.}, FJOURNAL = {Theoretical Computer Science}, VOLUME = {212}, YEAR = {1999}, NUMBER = {1-2}, PAGES = {183--209}, ISSN = {0304-3975}, CODEN = {TCSDI}, } @incollection {honsleni93, AUTHOR = {Honsell, Furio and Lenisa, Marina}, TITLE = {Some results on the full abstraction problem for restricted lambda calculi}, BOOKTITLE = {Mathematical foundations of computer science 1993 (Gda\'nsk, 1993)}, PAGES = {84--104}, PUBLISHER = {Springer}, ADDRESS = {Berlin}, YEAR = {1993}, } @article {dezadelipipe98, AUTHOR = {Dezani-Ciancaglini, Mariangiola and de'Liguoro, Ugo and Piperno, Adolfo}, TITLE = {A filter model for concurrent $\lambda$-calculus}, JOURNAL = {SIAM J. Comput.}, FJOURNAL = {SIAM Journal on Computing}, VOLUME = {27}, YEAR = {1998}, NUMBER = {5}, PAGES = {1376--1419 (electronic)}, ISSN = {1095-7111}, } @article {barbadezadeli95, AUTHOR = {Barbanera, Franco and Dezani-Ciancaglini, Mariangiola and de'Liguoro, Ugo}, TITLE = {Intersection and union types: syntax and semantics}, JOURNAL = {Inform. and Comput.}, FJOURNAL = {Information and Computation}, VOLUME = {119}, YEAR = {1995}, NUMBER = {2}, PAGES = {202--230}, ISSN = {0890-5401}, } @article {dezadelipipe96, AUTHOR = {Dezani-Ciancaglini, Mariangiola and de'Liguoro, Ugo and Piperno, Adolfo}, TITLE = {Filter models for conjunctive-disjunctive $\lambda$-calculi}, JOURNAL = {Theoret. Comput. Sci.}, FJOURNAL = {Theoretical Computer Science}, VOLUME = {170}, YEAR = {1996}, NUMBER = {1-2}, PAGES = {83--128}, ISSN = {0304-3975}, CODEN = {TCSDI}, } @article {abra91, AUTHOR = {Abramsky, Samson}, TITLE = {Domain theory in logical form}, NOTE = {Second Annual IEEE Symposium on Logic in Computer Science (Ithaca, NY, 1987)}, JOURNAL = {Ann. Pure Appl. Logic}, FJOURNAL = {Annals of Pure and Applied Logic}, VOLUME = {51}, YEAR = {1991}, NUMBER = {1-2}, PAGES = {1--77}, ISSN = {0168-0072}, CODEN = {APALD7}, } @article {abraong93, AUTHOR = {Abramsky, Samson and Ong, C.-H. Luke}, TITLE = {Full abstraction in the lazy lambda calculus}, JOURNAL = {Inform. and Comput.}, FJOURNAL = {Information and Computation}, VOLUME = {105}, YEAR = {1993}, NUMBER = {2}, PAGES = {159--267}, ISSN = {0890-5401}, } @incollection {ales94, AUTHOR = {Alessi, Fabio}, TITLE = {Type preorders}, BOOKTITLE = {Trees in algebra and programming---CAAP '94 (Edinburgh, 1994)}, PAGES = {37--51}, PUBLISHER = {Springer}, ADDRESS = {Berlin}, YEAR = {1994}, } @book {amadcuri98, AUTHOR = {Amadio, Roberto M. and Curien, Pierre-Louis}, TITLE = {Domains and lambda-calculi}, PUBLISHER = {Cambridge University Press}, ADDRESS = {Cambridge}, YEAR = {1998}, PAGES = {xvi+484}, ISBN = {0-521-62277-8}, } @article {bake96, AUTHOR = {van Bakel, Steffen}, TITLE = {Rank $2$ intersection type assignment in term rewriting systems}, JOURNAL = {Fund. Inform.}, FJOURNAL = {Fundamenta Informaticae}, VOLUME = {26}, YEAR = {1996}, NUMBER = {2}, PAGES = {141--166}, ISSN = {0169-2968}, CODEN = {FUINE}, } @article {bake92, AUTHOR = {van Bakel, Steffen}, TITLE = {Complete restrictions of the intersection type discipline}, JOURNAL = {Theoret. Comput. Sci.}, FJOURNAL = {Theoretical Computer Science}, VOLUME = {102}, YEAR = {1992}, NUMBER = {1}, PAGES = {135--163}, ISSN = {0304-3975}, CODEN = {TCSDI}, } @article {bake93, AUTHOR = {van Bakel, Steffen}, TITLE = {Principal type schemes for the strict type assignment system}, JOURNAL = {J. Logic Comput.}, FJOURNAL = {Journal of Logic and Computation}, VOLUME = {3}, YEAR = {1993}, NUMBER = {6}, PAGES = {643--670}, ISSN = {0955-792X}, } @article {bake95, AUTHOR = {van Bakel, Steffen}, TITLE = {Intersection type assignment systems}, NOTE = {Thirteenth Conference on Foundations of Software Technology and Theoretical Computer Science (Bombay, 1993)}, JOURNAL = {Theoret. Comput. Sci.}, FJOURNAL = {Theoretical Computer Science}, VOLUME = {151}, YEAR = {1995}, NUMBER = {2}, PAGES = {385--435}, ISSN = {0304-3975}, CODEN = {TCSDI}, } @article{barbmart94, AUTHOR = {Barbanera, Franco and Martini, Simone}, TITLE = {Proof-functional connectives and realizability}, JOURNAL = {Arch. Math. Logic}, FJOURNAL = {Archive for Mathematical Logic}, VOLUME = {33}, YEAR = {1994}, NUMBER = {3}, PAGES = {189--211}, ISSN = {0933-5846}, CODEN = {AMLOEH}, } @article {dezaghilvenn97, AUTHOR = {Dezani-Ciancaglini, Mariangiola and Ghilezan, Silvia and Venneri, Betti}, TITLE = {The ``relevance'' of intersection and union types}, JOURNAL = {Notre Dame J. Formal Logic}, FJOURNAL = {Notre Dame Journal of Formal Logic}, VOLUME = {38}, YEAR = {1997}, NUMBER = {2}, PAGES = {246--269}, ISSN = {0029-4527}, CODEN = {NDJFAM}, } @article {bohmdeza75, AUTHOR = {B{\"o}hm, Corrado and Dezani-Ciancaglini, Mariangiola}, TITLE = {$\lambda $-terms as total or partial functions on normal forms}, BOOKTITLE = {$\lambda $-calculus and computer science theory (Proc. Sympos., Rome, 1975)}, PAGES = {96--121. Lecture Notes in Comput. Sci., Vol. 37}, PUBLISHER = {Springer}, ADDRESS = {Berlin}, YEAR = {1975}, } article {dezamarg86, AUTHOR = {Dezani-Ciancaglini, Mariangiola and Margaria, Ines}, TITLE = {A characterization of ${F}$-complete type assignments}, JOURNAL = {Theoret. Comput. Sci.}, FJOURNAL = {Theoretical Computer Science}, VOLUME = {45}, YEAR = {1986}, NUMBER = {2}, PAGES = {121--157}, ISSN = {0304-3975}, CODEN = {TCSDI}, } @article {carddezadeli94, AUTHOR = {Cardone, Felice and Dezani-Ciancaglini, Mariangiola and de'Liguoro, Ugo}, TITLE = {Combining type disciplines}, JOURNAL = {Ann. Pure Appl. Logic}, FJOURNAL = {Annals of Pure and Applied Logic}, VOLUME = {66}, YEAR = {1994}, NUMBER = {3}, PAGES = {197--230}, ISSN = {0168-0072}, CODEN = {APALD7}, } @article {boud94, AUTHOR = {Boudol, G{\'e}rard}, TITLE = {Lambda-calculi for (strict) parallel functions}, JOURNAL = {Inform. and Comput.}, FJOURNAL = {Information and Computation}, VOLUME = {108}, YEAR = {1994}, NUMBER = {1}, PAGES = {51--127}, ISSN = {0890-5401}, } @article {comppier96, AUTHOR = {Compagnoni, Adriana B. and Pierce, Benjamin C.}, TITLE = {Higher-order intersection types and multiple inheritance}, JOURNAL = {Math. Structures Comput. Sci.}, FJOURNAL = {Mathematical Structures in Computer Science. A Journal in the Applications of Categorical, Algebraic and Geometric Methods in Computer Science}, VOLUME = {6}, YEAR = {1996}, NUMBER = {5}, PAGES = {469--501}, ISSN = {0960-1295}, } @article {comp96, AUTHOR = {Compagnoni, Adriana B. and Pierce, Benjamin C.}, TITLE = {Higher-order intersection types and multiple inheritance}, JOURNAL = {Math. Structures Comput. Sci.}, FJOURNAL = {Mathematical Structures in Computer Science. A Journal in the Applications of Categorical, Algebraic and Geometric Methods in Computer Science}, VOLUME = {6}, YEAR = {1996}, NUMBER = {5}, PAGES = {469--501}, ISSN = {0960-1295}, } @incollection {digihons93, AUTHOR = {Di Gianantonio, Pietro and Honsell, Furio}, TITLE = {An abstract notion of application}, BOOKTITLE = {Typed lambda calculi and applications (Utrecht, 1993)}, PAGES = {124--138}, PUBLISHER = {Springer}, ADDRESS = {Berlin}, YEAR = {1993}, } @article {egidhonsronc92, AUTHOR = {Egidi, Lavinia and Honsell, Furio and Ronchi Della Rocca, Simona}, TITLE = {Operational, denotational and logical descriptions: a case study}, NOTE = {Mathematical foundations of computer science '91 (Kazimierz Dolny, 1991)}, JOURNAL = {Fund. Inform.}, FJOURNAL = {Fundamenta Informaticae}, VOLUME = {16}, YEAR = {1992}, NUMBER = {2}, PAGES = {149--169}, ISSN = {0169-2968}, CODEN = {FUINE8}, } @article {gira88, AUTHOR = {Girard, Jean-Yves}, TITLE = {Normal functors, power series and $\lambda$-calculus}, JOURNAL = {Ann. Pure Appl. Logic}, FJOURNAL = {Annals of Pure and Applied Logic}, VOLUME = {37}, YEAR = {1988}, NUMBER = {2}, PAGES = {129--177}, ISSN = {0168-0072}, CODEN = {APALD7}, } @article {enge81, AUTHOR = {Engeler, Erwin}, TITLE = {Algebras and combinators}, JOURNAL = {Algebra Universalis}, FJOURNAL = {Algebra Universalis}, VOLUME = {13}, YEAR = {1981}, NUMBER = {3}, PAGES = {389--392}, ISSN = {0002-5240}, } @article {ghil96, AUTHOR = {Ghilezan, Silvia}, TITLE = {Strong normalization and typability with intersection types}, JOURNAL = {Notre Dame J. Formal Logic}, FJOURNAL = {Notre Dame Journal of Formal Logic}, VOLUME = {37}, YEAR = {1996}, NUMBER = {1}, PAGES = {44--52}, ISSN = {0029-4527}, CODEN = {NDJFAM}, } @incollection {hind82, AUTHOR = {Hindley, J. R.}, TITLE = {The simple semantics for {C}oppo--{D}ezani--{S}all\'e types}, BOOKTITLE = {International symposium on programming (Turin, 1982)}, PAGES = {212--226}, PUBLISHER = {Springer}, ADDRESS = {Berlin}, YEAR = {1982}, } @article {hindlong80, AUTHOR = {Hindley, R. and Longo, G.}, TITLE = {Lambda-calculus models and extensionality}, JOURNAL = {Z. Math. Logik Grundlag. Math.}, FJOURNAL = {Zeitschrift f\"ur Mathematische Logik und Grundlagen der Mathematik}, VOLUME = {26}, YEAR = {1980}, NUMBER = {4}, PAGES = {289--310}, ISSN = {0044-3050}, CODEN = {ZMLGAQ}, } @article {hind94, AUTHOR = {Hindley, J. Roger}, TITLE = {Coppo\mhy {D}ezani types do not correspond to propositional logic}, JOURNAL = {Theoret. Comput. Sci.}, FJOURNAL = {Theoretical Computer Science}, VOLUME = {28}, YEAR = {1984}, NUMBER = {1-2}, PAGES = {235--236}, ISSN = {0304-3975}, CODEN = {TCSDI}, } @article {honsronc92, AUTHOR = {Honsell, Furio and Ronchi Della Rocca, Simona}, TITLE = {An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus}, JOURNAL = {J. Comput. System Sci.}, FJOURNAL = {Journal of Computer and System Sciences}, VOLUME = {45}, YEAR = {1992}, NUMBER = {1}, PAGES = {49--75}, ISSN = {0022-0000}, CODEN = {JCSSBM}, } @book {john86, AUTHOR = {Johnstone, Peter T.}, TITLE = {Stone spaces}, NOTE = {Reprint of the 1982 edition}, PUBLISHER = {Cambridge University Press}, ADDRESS = {Cambridge}, YEAR = {1986}, PAGES = {xxii+370}, ISBN = {0-521-33779-8}, } @article {leiv86, AUTHOR = {Leivant, Daniel}, TITLE = {Typing and computational properties of lambda expressions}, JOURNAL = {Theoret. Comput. Sci.}, FJOURNAL = {Theoretical Computer Science}, VOLUME = {44}, YEAR = {1986}, NUMBER = {1}, PAGES = {51--68}, ISSN = {0304-3975}, CODEN = {TCSDI}, } @incollection {lope85, AUTHOR = {L{\'o}pez-Escobar, E. G. K.}, TITLE = {Proof functional connectives}, BOOKTITLE = {Methods in mathematical logic (Caracas, 1983)}, PAGES = {208--221}, PUBLISHER = {Springer}, ADDRESS = {Berlin}, YEAR = {1985}, } @article {margzacc95, AUTHOR = {Margaria, Ines and Zacchi, Maddalena}, TITLE = {Principal typing in a $\forall\wedge$-discipline}, JOURNAL = {J. Logic Comput.}, FJOURNAL = {Journal of Logic and Computation}, VOLUME = {5}, YEAR = {1995}, NUMBER = {3}, PAGES = {367--381}, ISSN = {0955-792X}, } @article {meye82, AUTHOR = {Meyer, Albert R.}, TITLE = {What is a model of the lambda calculus?}, JOURNAL = {Inform. and Control}, FJOURNAL = {Information and Control}, VOLUME = {52}, YEAR = {1982}, NUMBER = {1}, PAGES = {87--122}, ISSN = {0019-9958}, CODEN = {IFCNA4}, } @TechReport{meye95, author = "Meyer, R.K.", title = "Types and the Boolean System {\bf CB}$^+$", institution = "ANU University", year = "1995", OPTcrossref = "", OPTkey = "", OPTtype = "", OPTnumber = "", address = "Canberra", OPTmonth = "", note = "ARP Technical Report TR-SRS-5-95", OPTannote = "" } article {pier97, AUTHOR = {Pierce, Benjamin C.}, TITLE = {Intersection types and bounded polymorphism}, JOURNAL = {Math. Structures Comput. Sci.}, FJOURNAL = {Mathematical Structures in Computer Science. A Journal in the Applications of Categorical, Algebraic and Geometric Methods in Computer Science}, VOLUME = {7}, YEAR = {1997}, NUMBER = {2}, PAGES = {129--193}, ISSN = {0960-1295}, } @article {plot75, AUTHOR = {Plotkin, G. D.}, TITLE = {Call-by-name, call-by-value and the $\lambda $-calculus}, JOURNAL = {Theoret. Comput. Sci.}, VOLUME = {1}, YEAR = {1975}, NUMBER = {2}, PAGES = {125--159}, } @article {plot93, AUTHOR = {Plotkin, Gordon D.}, TITLE = {Set-theoretical and other elementary models of the $\lambda$-calculus}, NOTE = {A collection of contributions in honour of Corrado B\"ohm on the occasion of his 70th birthday}, JOURNAL = {Theoret. Comput. Sci.}, FJOURNAL = {Theoretical Computer Science}, VOLUME = {121}, YEAR = {1993}, NUMBER = {1-2}, PAGES = {351--409}, ISSN = {0304-3975}, CODEN = {TCSDI}, } article {plot94, AUTHOR = {Plotkin, Gordon}, TITLE = {A semantics for static type inference}, NOTE = {International Conference on Theoretical Aspects of Computer Software (TACS '91) (Sendai, 1991)}, JOURNAL = {Inform. and Comput.}, FJOURNAL = {Information and Computation}, VOLUME = {109}, YEAR = {1994}, NUMBER = {1-2}, PAGES = {256--299}, ISSN = {0890-5401}, }@incollection {pott80, AUTHOR = {Pottinger, Garrel}, TITLE = {A type assignment for the strongly normalizable $\lambda $-terms}, BOOKTITLE = {To H. B. Curry: essays on combinatory logic, lambda calculus and formalism}, PAGES = {561--577}, PUBLISHER = {Academic Press}, ADDRESS = {London}, YEAR = {1980}, } @incollection {reyn89, AUTHOR = {Reynolds, John C.}, TITLE = {Syntactic control of interference. {I}{I}}, BOOKTITLE = {Automata, languages and programming (Stresa, 1989)}, PAGES = {704--722}, PUBLISHER = {Springer}, ADDRESS = {Berlin}, YEAR = {1989}, } @incollection {reyn91, AUTHOR = {Reynolds, John C.}, TITLE = {The coherence of languages with intersection types}, BOOKTITLE = {Theoretical aspects of computer software (Sendai, 1991)}, PAGES = {675--700}, PUBLISHER = {Springer}, ADDRESS = {Berlin}, YEAR = {1991}, } @article {MR90k:03014, AUTHOR = {Ronchi Della Rocca, Simona}, TITLE = {Principal type scheme and unification for intersection type discipline}, NOTE = {International Joint Conference on Theory and Practice of Software Development (Pisa, 1987)}, JOURNAL = {Theoret. Comput. Sci.}, FJOURNAL = {Theoretical Computer Science}, VOLUME = {59}, YEAR = {1988}, NUMBER = {1-2}, PAGES = {181--209}, ISSN = {0304-3975}, CODEN = {TCSDI}, } @article {roncvenn84, AUTHOR = {Ronchi Della Rocca, S. and Venneri, B.}, TITLE = {Principal type schemes for an extended type theory}, JOURNAL = {Theoret. Comput. Sci.}, FJOURNAL = {Theoretical Computer Science}, VOLUME = {28}, YEAR = {1984}, NUMBER = {1-2}, PAGES = {151--169}, ISSN = {0304-3975}, CODEN = {TCSDI}, } @incollection {sanc80, AUTHOR = {Sanchis, Luis E.}, TITLE = {Reflexive domains}, BOOKTITLE = {To H. B. Curry: essays on combinatory logic, lambda calculus and formalism}, PAGES = {339--361}, PUBLISHER = {Academic Press}, ADDRESS = {London}, YEAR = {1980}, } @incollection {scot72, AUTHOR = {Scott, Dana}, TITLE = {Continuous lattices}, BOOKTITLE = {Toposes, algebraic geometry and logic (Conf., Dalhousie Univ., Halifax, N. S., 1971)}, PAGES = {97--136. Lecture Notes in Math., Vol. 274}, PUBLISHER = {Springer}, ADDRESS = {Berlin}, YEAR = {1972}, } @article {scot76, AUTHOR = {Scott, Dana}, TITLE = {Data types as lattices}, OPTNOTE = {Semantics and correctness of programs}, JOURNAL = {SIAM J. Comput.}, VOLUME = {5}, YEAR = {1976}, NUMBER = {3}, PAGES = {522--587}, } @incollection {MR83m:68029, AUTHOR = {Scott, Dana S.}, TITLE = {Domains for denotational semantics}, BOOKTITLE = {Automata, languages and programming (Aarhus, 1982)}, PAGES = {577--613}, PUBLISHER = {Springer}, ADDRESS = {Berlin}, YEAR = {1982}, } @article {venn94, AUTHOR = {Venneri, Betti}, TITLE = {Intersection types as logical formulae}, JOURNAL = {J. Logic Comput.}, FJOURNAL = {Journal of Logic and Computation}, VOLUME = {4}, YEAR = {1994}, NUMBER = {2}, PAGES = {109--124}, ISSN = {0955-792X}, } @book {vick89, AUTHOR = {Vickers, Steven}, TITLE = {Topology via logic}, PUBLISHER = {Cambridge University Press}, ADDRESS = {Cambridge}, YEAR = {1989}, PAGES = {xvi+200}, ISBN = {0-521-36062-5}, } @incollection {MR99i:03015, AUTHOR = {Yokouchi, Hirofumi}, TITLE = {Completeness of type assignment systems with intersection, union, and type quantifiers}, BOOKTITLE = {Thirteenth Annual IEEE Symposium on Logic in Computer Science (Indianapolis, IN, 1998)}, PAGES = {368--379}, PUBLISHER = {IEEE Computer Soc., Los Alamitos, CA}, YEAR = {1998}, } @STRING{archiv = {Archiv f\"ur Mathematische Logik und Grundlagenforschung}} @STRING{joSL = {Journal of Symbolic Logic}} @STRING{LNiM = {Lecture Notes in Mathematics}} @STRING{academicp = {Academic Press}} % NY @STRING{addison = {Addison-Wesley}} % Reading, MA @STRING{birkhauser = {Birkhauser}} % Boston, MA @STRING{cup = {Cambridge University Press}} @STRING{csp = {Computer Science Press}} % Rockville, MD @STRING{dover = {Dover Publications, Inc.}} % NY @STRING{freeman = {W. H. Freeman and Co.}} % San Francisco, CA @STRING{holt = {Holt, Rinehart and Winston}} % NY @STRING{hopkins = {The Johns Hopkins U. Press}} % Baltimore, MD @STRING{macmillan = {Macmillan Publishing Co., Inc.}} % NY @STRING{mcgraw = {McGraw-Hill Book Co.}} % NY @STRING{mitp = {MIT Press}} % Cambridge, MA @STRING{nholland = {North-Holland}} % NY @STRING{prentice = {Prentice-Hall International. Englewood Cliffs, NJ}} @STRING{princeton = {Princeton U. Press}} % Princeton, NJ @STRING{springer = {Springer-Verlag}} % NY @STRING{wiley = {John Wiley \& Sons}} % NY @STRING{yale = {Yale U. Press}} % New Haven, CT @STRING{ny = {New York}} @INCOLLECTION{spec62 , AUTHOR = "C. Spector" , TITLE = "Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics" , BOOKTITLE = "Recursive function theory, Proc. Symp. in pure mathematics V" , EDITOR = "J.C.E. Dekker" , PUBLISHER = "AMS" , ADDRESS = "Providence" , PAGES = "1--27" , YEAR = 1962 , STATUS = "not in possession"} @BOOK{troe73 , AUTHOR = {A.S. Troelstra} , TITLE = {Metamathematical Investigation of Intuitionistic Arithmetic and Analysis} , SERIES = LNiM , NUMBER = 344 , PUBLISHER = springer , ADDRESS = {Berlin} , CROSSREFONLY = 1 , YEAR = 1973 , STATUS = {in possession of M.A. Bezem}} @ARTICLE{goed58 , AUTHOR = {K. G\"{o}del} , TITLE = {Ueber eine bisher noch nicht ben\"{u}tzte {E}rweiterung des finiten {S}tandpunktes} , JOURNAL = {Dialectica} , VOLUME = 12 , PAGES = "280--287" , YEAR = 1958 , STATUS = "in possession"} @ARTICLE{beze85a , AUTHOR = {M.A. Bezem} , TITLE = {Strongly majorizable functionals of finite type: a model for bar recursion containing discontinuous functionals} , JOURNAL = JoSL , VOLUME = 50 , PAGES = "652--660" , YEAR = 1985 , STATUS = "in possession"} @article{beze85, author = "M.A. Bezem", title = "Strong normalization of bar recursive terms without using infinite terms", journal = archiv, volume = 25, year = 1985, pages = "175--181" } @ARTICLE{voge76 , AUTHOR = {H. Vogel} , TITLE = {Ein starker {N}ormalisationssatz f\"ur die barrekursiven {F}unktionale} , JOURNAL = archiv , VOLUME = 18 , PAGES = "81--84" , YEAR = 1976 , STATUS = "in possession"} @BOOK{luck73 , AUTHOR = {H. Luckhardt} , TITLE = {Extensional G\"odel functional interpretation} , SERIES = LNiM , NUMBER = 306 , PUBLISHER = springer , ADDRESS = {Berlin} , CROSSREFONLY = 1 , YEAR = 1973 , STATUS = {in possession of M.A. Bezem}} @INCOLLECTION{tait71 , AUTHOR = {Tait, W.W.} , TITLE = {Normal form theorem for barrecursive functions of finite type} , BOOKTITLE = "Proceedings of the 2nd {S}candinavian Logic Symposium" , EDITOR = "Fenstad, J.E." , PAGES = "353--367" , PUBLISHER = nholland , ADDRESS = "Amsterdam" , YEAR = 1971} @BOOK{pete67 , AUTHOR = {R. P\'eter} , TITLE = {Recursive functions} , PUBLISHER = academicp , ADDRESS = {New York} , YEAR = 1967 , edition = "Third revised edition"} @ARTICLE{plot77 , AUTHOR = {G. Plotkin} , TITLE = {{LCF} considered as a programming language} , JOURNAL = tcs , VOLUME = 5 , PAGES = "xx--xx" , YEAR = 1977} @phdthesis{plat66 , AUTHOR = {R.A. Platek} , TITLE = {Foundations of recursions theory} , SCHOOL = {Stanford University} , YEAR = 1966} @PHDTHESIS{raam96, AUTHOR = "Raamsdonk, F. van", TITLE = "Confluence and Normalisation for Higher-Order Rewriting", SCHOOL = "Vrije Universiteit", YEAR = 1996, ADDRESS = "Amsterdam, The Netherlands", MONTH = may } %%Refbook3.bib @inproceedings{dezahonsales00, author={Dezani-Ciancaglini, Mariangiola and Honsell, Furio and Alessi, Fabio}, title={A complete characterization of the complete intersection-type theories}, booktitle={ICALP Workshops 2000}, editor={Rolim, J. and Broder, A. and Corradini, A. and Gorrieri, R. and Heckel, R. and Hromkovic, J. and Vaccaro, U. and Wells, J.}, publisher={Carleton-Scientific}, series={Proceedings in Informatics 8}, address={Canada}, year={2000}, PAGES = {287--302}, } @article {hind83, AUTHOR = {Hindley, J.Roger}, TITLE = {The completeness theorem for typing $\lambda$-terms}, JOURNAL = {Theoret. Comput. Sci.}, FJOURNAL = {Theoretical Compututer Science}, VOLUME = {22}, YEAR = {1983}, PAGES = {1--17}, } @article {hind83a, AUTHOR = {Hindley, J.Roger}, TITLE = {The completeness theorem for typing $\lambda$-terms}, JOURNAL = {Theoret. Comput. Sci.}, FJOURNAL = {Theoretical Compututer Science}, VOLUME = {22}, YEAR = {1983}, PAGES = {127--133}, } @article {yoko94, AUTHOR = {Yokouchi, Hirofumi}, TITLE = {F-semantics for type assignment systems}, JOURNAL = {Theoret. Comput. Sci.}, FJOURNAL = {Theoretical Compututer Science}, VOLUME = {129}, YEAR = {1994}, PAGES = {39-77}, } @unpublished{scot80l, author = {Scott, Dana S.}, title = {Letter to {A}lbert {M}eyer}, year = {1980}, note = {CMU} } @unpublished{venn96, author = {Venneri, Betti}, title = {Private Communication}, year = {1996}, note = {Florence University} } @Book{mitc96, author = {Mitchell, John}, title = {Foundation for Programmimg Languages}, publisher = {MIT Press}, year = {1996} } @article {mitc88, AUTHOR = {Mitchell, John}, TITLE = {Polymorphic type inference and containment}, JOURNAL = {Inform. and Comput.}, FJOURNAL = {Information and Computation}, VOLUME = {76}, YEAR = {1988}, PAGES = {211--249}, } @unpublished{mart83, AUTHOR = {Martin-L\"of, Per}, TITLE = {Lecture notes on domain interpretation of type theory}, year = {1983}, note = {Programming {M}ethodology {G}roup, Workshop on the Semantics of Programming Languages, Chalmers University of Technology}, } @article {long83, AUTHOR = {Longo, Giuseppe}, TITLE = {Set-theoretical models of $\lambda $-calculus: theories, expansions, isomorphisms}, JOURNAL = {Ann. Pure Appl. Logic}, FJOURNAL = {Annals of Pure and Applied Logic}, VOLUME = {24}, YEAR = {1983}, NUMBER = {2}, PAGES = {153--188}, ISSN = {0168-0072}, CODEN = {APALD7}, } @incollection {scot82, AUTHOR = {Scott, Dana S.}, TITLE = {Domains for denotational semantics}, BOOKTITLE = {Automata, languages and programming (Aarhus, 1982)}, PAGES = {577--613}, PUBLISHER = {Springer}, ADDRESS = {Berlin}, YEAR = {1982}, } @unpublished{ales93, author = {Alessi, Fabio}, title = {The p model}, year = {1993}, note = {Internal Report, Udine University}, } @PhdThesis{seve96, author = "Severi, Paula", title = "Normalisation in lambda calculus and its relation to type inference", school = "Eindhoven University of Technology", year = "1996" } @article {ronc88, AUTHOR = {Ronchi Della Rocca, Simona}, TITLE = {Lecture Notes on Semantics and Types}, year = "1988", note = {Internal Report, Torino University}, } @incollection {jaco75, AUTHOR = {Jacopini, Giuseppe}, TITLE = {A condition for identifying two elements of whatever model of combinatory logic}, BOOKTITLE = {$\lambda $-calculus and computer science theory (Proc. Sympos., Rome, 1975)}, PAGES = {213--219. Lecture Notes in Comput. Sci., Vol. 37}, PUBLISHER = {Springer}, ADDRESS = {Berlin}, YEAR = {1975}, } @article {baetboer79, AUTHOR = {Baeten, J. and Boerboom,B.}, TITLE = {$\Omega$ can be anything it shouldn't be}, JOURNAL = {Indag.Math.}, VOLUME = {41}, YEAR = {1979}, PAGES = {111--120}, } @article {dezamarg86, AUTHOR = {Dezani-Ciancaglini, Mariangiola and Margaria, Ines}, TITLE = {A characterization of ${F}$-complete type assignments}, JOURNAL = {Theoret. Comput. Sci.}, FJOURNAL = {Theoretical Computer Science}, VOLUME = {45}, YEAR = {1986}, NUMBER = {2}, PAGES = {121--157}, ISSN = {0304-3975}, CODEN = {TCSDI}, } %%%%AAAA @article{acke28, author={Ackermann, W.}, title={Zum Hilbertschen Aufbau der reellen Zahlen}, journal={Mathematische Annalen}, year=1928, volume=99, pages={118--133} } @book{abragabbmaib92, editor="Abramsky, S. and Gabbay, Dov M. and Maibaum, T.S.E.", title={Handbook of Logic in Computer Science, Volume 2: Background: Computational Structures}, year={1992}, publisher={Oxford Science Publications}, tue={wis cbk 92 han} } @inproceedings{acze78, author={Aczel, P.}, title={The type theoretic interpretation of constructive set theory}, booktitle={Logic Colloquium '77}, note={Studies in Logic and the Foundations of Mathematics {\bf 96}}, editor="Macintyre, A. and Pacholski, L. and Paris, J.", publisher={North-Holland}, address={Amsterdam}, year={1978}, tue={wis cbl 71 log} } @inproceedings{acze80, author={Aczel, P.}, title={Frege structures and the notion of proposition, truth and set}, booktitle={The Kleene Symposium}, note={Studies in Logic and the Foundations of Mathematics {\bf 101}}, editor="Barwise, J. and Keisler, H. and Kunen, K.", publisher={North-Holland}, address={Amsterdam}, year={1980}, tue={wis cbn 80 kle} } @article{ajdu35, author={Ajdukiewicz, K.}, title={Die syntaktische {K}onnexit\"at}, journal={Studia Philosophica}, volume={1}, pages={1--27}, year={1935}, note={in German; English translation in \cite{mcca67}}, tue={Zie mcca67} } @mastersthesis{aleb94, author={Alebeek, E. van}, title={Isomorfie van beslisbare en opsombare ondergroepen van $(\q,+)$}, school={Department of Mathematics, Catholic University Nijmegen}, year={1994}, note={Dutch}, tue={IN BEZIT} } @incollection {alesbarb91, AUTHOR = {Alessi, Fabio and Barbanera, Franco}, TITLE = {Strong conjunction and intersection types}, BOOKTITLE = {Mathematical foundations of computer science, 1991 (Kazimierz Dolny, 1991)}, PAGES = {64--73}, PUBLISHER = {Springer}, ADDRESS = {Berlin}, YEAR = {1991}, } @PhdThesis{ales91, author = "Alessi, Fabio", title = "Strutture di tipi, teoria dei domini e modelli del lambda calcolo", school = "Torino University", year = "1991", OPTcrossref = "", OPTkey = "", address = "", OPTmonth = "", OPTtype = "", OPTnote = "", OPTannote = "" } BBBB @techreport{baetmauw94, author="Baeten, J.C.M. and Mauw, S.", title={Delayed Choice: An Operator for Joining Message Sequence Charts} , year={1994}, number={35}, institution={TUE Computing Science Reports}, address={Eindhoven University of Technology}, tue={IN BEZIT} } @article{barb95, author={Barbanera, Franco and Mariangiola Dezani--Ciancaglini and Ugo de' Liguoro}, title={Intersection and union types: syntax and semantics}, journal={Information and Computation}, volume={119}, pages={202--230}, year={1995}, } @incollection{bare92, author={Barendregt, Henk P.}, year={1992}, title={Lambda Calculi with types}, booktitle={{\rm\cite{abragabbmaib92}}}, publisher={Oxford University Press}, pages={117--309}, tue={wis CBK 92 HAN} } @incollection{bare96, author={Barendregt, H.P.}, year={1996}, title={The quest for correctness}, booktitle={Images of SMC Research}, publisher={Stichting Mathematisch Centrum}, address={P.O. Box 94079, 1090 GB Amsterdam}, pages={39--58} } @article{dekkbundbare97, author="Dekkers, W. and Bunder, M. and Barendregt, H.P.", title={Completeness of the propositions-as-types interpretation of intuitionistic logic into illative combinatory logic}, year={1997}, journal={The Journal of Symbolic Logic}, volume={To appear}, number={}, pages={}, tue={IN BEZIT} } @book{barwmoss96, author="Barwise, J. and Moss, L.", title="Vicious Circles", year={1996}, address={Stanford}, publisher={CSLI Publications}, tue={wis ...} } @book{benaputn83, editor="Benacerraf, P. and Putnam, H.", title={Philosophy of Mathematics}, publisher={Cambridge University Press}, year={1983}, edition={second}, tue={wis cbd 83 phi} } @article{bent78, author="Benthem, J.F.A.K. van", title="Four Paradoxes", year={1978}, journal="Journal of Philosophical Logic", volume="7", pages="49--72", tue={IN BEZIT} } @book{bent91, author={Benthem, J.F.A.K. van}, title={Language in Action: Categories, Lambdas and Dynamic Logic}, publisher={North-Holland}, year={1991}, series={Studies in Logic and the Foundations of Mathematics {\bf 130}}, address={Amsterdam}, tue={IN BEZIT} } @techreport{btjt81, author={Benthem Jutting, L.S. van}, title={Description of {A}{U}{T}-68}, year={1981}, number={12}, institution={Eindhoven University of Technology}, note={also in \cite{nedegeuvvrij94}}, tue={IN BEZIT} } @techreport{bera88, author={Berardi, S.}, title={Towards a mathematical analysis of the {C}oquand-{H}uet calculus of constructions and the other systems in {B}arendregt's cube}, year={1988}, institution={Dept. of Computer Science, Carnegie-Mellon University and Dipartimento Matematica, Universita di Torino}, tue={...} } @phdthesis{bera90, author={Berardi, S.}, title={Type Dependence and Constructive Mathematics}, year={1990}, school={Dipartimento Matematica}, address={Universit\`a di Torino}, tue={...} } @techreport{berabezecoqu94, author="Berardi, S. and Bezem, M.A. and Coquand, T.", title={On the computational content of the Axiom of Choice}, year={1994}, number={116}, institution={Department of Philosophy, Utrecht University}, tue={IN BEZIT} } @book{bergklopmidd89, author="Bergstra, J.A. and Klop, J.W. and Middeldorp, A.", title={Termherschrijfsystemen}, publisher={Kluwer Programmatuurkunde}, year={1989}, note={Dutch}, tue={wis dbn 89 ber} } @book{beth59, author={Beth, E.W.}, title={The Foundations of Mathematics}, publisher={North-Holland}, year={1959}, series={Studies in Logic and the Foundations of Mathematics}, address={Amsterdam}, tue={wis cbb 59 bet} } @mastersthesis{blee95, author={Bleeker, A.}, title={An Approach to Image Retrieval}, year={1995}, school={Katholieke Universiteit Nijmegen/Universit\`a di Padova}, tue={IN BEZIT} } @mastersthesis{bloo93, author={Bloo, R.}, title={Over de begrippen gefundeerd en verstrooid}, year={1993}, school={Department of Mathematics, Catholic University Nijmegen}, note={Dutch}, tue={IN BEZIT} } @techreport{bloo95, author={Bloo, R.}, title={Preservation of Strong Normalisation for Explicit Substitution}, institution={TUE Computing Science Notes}, address={Eindhoven University of Technology}, number={8}, year={1995}, month={mar}, tue={IN BEZIT} } @techreport{blookamanede94, author="Bloo, R. and Kamareddine, F. and Nederpelt, R.", title={Beyond $\beta$-Reduction in {C}hurch's $\lambda{\rightarrow}$}, institution={TUE Computing Science Notes}, address={Eindhoven University of Technology}, number={20}, year={1994}, month={apr}, tue={IN BEZIT} } @techreport{blookamanede94a, author="Bloo, R. and Kamareddine, F. and Nederpelt, R.", title={The $\lambda$-cube with classes of terms modulo conversion}, institution={TUE Computing Science Reports}, address={Eindhoven University of Technology}, number={46}, year={1994}, tue={IN BEZIT} } @techreport{blookamanede94b, author={Bloo, R. and Kamareddine, F. and Nederpelt, R.}, title={On {$\Pi$}-conversion in Type Theory}, institution={TUE Computing Science Reports}, address={Eindhoven University of Technology}, number={47}, year={1994}, tue={IN BEZIT} } @techreport{blookamanede94c, author={Bloo, R. and Kamareddine, F. and Nederpelt, R.}, title={The {B}arendregt {C}ube with {D}efinitions and {G}eneralised {R} eduction}, institution={TUE Computing Science Reports}, address={Eindhoven University of Technology}, number={34}, year={1994}, note={Also as Technical Report 8, University of Glasgow, Computing Science Department, 1994. To be published in Information and Computation}, tue={IN BEZIT} } @article{blookamanede95, author={Kamareddine, F. and Bloo, R. and Nederpelt, R.}, title={Definitions and {$\Pi$}-conversion in Type Theory}, year={1995}, journal={Submitted}, tue={Copie IN BEZIT} } @article{blookamanede96, author={Bloo, R. and Kamareddine, F. and Nederpelt, R.}, title={The {B}arendregt {C}ube with {D}efinitions and {G}eneralised {R}eduction}, year={1996}, journal={{I}nformation and {C}omputation}, volume={126}, number={2}, pages={123--143}, tue={IN BEZIT} } @phdthesis{borg94, author={Borghuis, V.A.J.}, title={Coming to Terms with Modal Logic: On the interpretation of modal ities in typed $\lambda$-calculus}, school={Technische Universiteit Eindhoven}, year={1994}, tue={IN BEZIT} } @phdthesis{boum93, author={Bouma, G.}, title={Nonmonotonicity and Categorial Unification Grammar}, school={Rijksuniversiteit Groningen}, year={1993}, tue={hfst. 1-3 in reader categoriale grammatica IN BEZIT} } @mastersthesis{bran95, author={Brands, J.}, title={Spelen met 0-1 wetten}, school={Department of Mathematics, Catholic University Nijmegen}, year={1995}, note={Dutch}, tue={IN BEZIT} } @mastersthesis{bron94, author={Bron, I.G.L.}, title={Benaderen van looptijden voor uittredingen die zich met zeer kle ine kans voordoen}, school={Department of Mathematics, Catholic University Nijmegen}, year={1994}, note={Dutch}, tue={IN BEZIT} } @phdthesis{brou07, author={{B}rouwer, L.E.J.}, title={Over de Grondslagen der Wiskunde}, school={Universiteit van Amsterdam}, year={1907}, note={Dutch; English translation in \cite{heyt75}}, tue={collected works: wis cae 75 bro; van dalen (ed): wis cbb 81 bro} } @article{brou18, author={Brouwer, L.E.J.}, title={Begr\"undung der {M}engenlehre unabh\"angig vom logischen {S}atz vom ausgeschlossenen {D}ritten}, journal={KNAW Verhandelingen}, year={1918}, volume={12}, number={5}, note={German; also in \cite{heyt75}}, tue={collected works: wis cae 75 bro} } @techreport{brui68, author={de Bruijn, N. G.}, title="{A}{U}{T}{O}{M}{A}{T}{H}, a language for mathematics", year={1968}, institution={T.H.-Reports}, number={68-{W}{S}{K}-05}, address={Eindhoven University of Technology}, tue={wis ARC 01 EUT} } @inproceedings{brui70, author={N. G. de Bruijn}, title={The mathematical language {A}{U}{T}{O}{M}{A}{T}{H}, its usage and some of its extensions}, booktitle={Symposium on Automatic Demonstration}, organization={Springer Verlag}, publisher={Berlin, 1970}, address={{I}{R}{I}{A}, Versailles}, editor="Laudet, M. and Lacombe, D. and Schuetzenberger, M.", pages={29--61}, year={1970}, note={Lecture Notes in Mathematics {\bf 125}; also in \cite{nedegeuvvrij94}}, tue={IN BEZIT} } @article {debr72, AUTHOR = {de Bruijn, N. G.}, TITLE = {Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the {C}hurch-{R}osser theorem}, JOURNAL = {Nederl. Akad. Wetensch. Proc. Ser. A {\bf 75}=Indag. Math.}, VOLUME = {34}, YEAR = {1972}, PAGES = {381--392}, } @inproceedings{debr68, author={N. G. de Bruijn}, title={The Mathematical Language {AUTOMATH}, Its Usage, and Some of Its Extensions}, editor={M. Laudet}, pages={29--61}, booktitle={Proceedings of the Symposium on Automatic Demonstratio n}, year={1968}, publisher={Springer-Verlag LNM 125}, address={Versailles, France}, month={dec}, keywords={Automath} } @techreport{brunkatokoymmauw93, author="Brunekreef, J. and Katoen, J.-P. and Koymans, R. and Mauw, S.", title={Design and Analysis of Dynamic Leader Election Protocols in Broa dcast Networks}, year={1993}, number={37}, institution={TUE Computing Science Notes}, address={Eindhoven University of Technology}, tue={IN BEZIT} } @article{bura97, author={Burali-Forti, C.}, title={Una questione su i numeri transfiniti}, year={1897}, journal={Rendiconti del Corcolo Matematico di Palermo}, volume={11}, note={English translation in \cite{heij67}, pages 104--112} } @article{burg86, author={Burgess, J.P.}, title={The Truth is Never Simple}, journal={Journal of Symbolic Logic}, volume={51}, pages={663--681}, year={1986}, tue={IN BEZIT} } @book{buszmarcbent88, editor="Buszkowski, W. and Marciszewski, W. and Benthem, J. van", title={Categorial Grammar}, publisher={John Benjamins}, year={1988}, series={Linguistic \&\ Literary Studies in Eastern Europe {\bf 25}}, address={Amsterdam}, tue={IPO-bibliotheek XF 88} } %CCCC @article{capr98, author={Capretta, V. and S. Valentini}, title={A general method for proving the normalization theorem for first and second order typed $\l$-calculi}, note={To appear}, journal={Mathematical Structures in Computer Science}, year={1998}, } @book{carn29, author={Carnap, R.}, title={Abriss der Logistik}, year={1929}, publisher={Springer Verlag}, address={Wien} } @book{carn65, author={Carnap, R.}, title={Foundations of Logic and Mathematics}, series={International Encyclopedia of Unified Science}, year={1965}, publisher={University of Chicago Press}, tue={wis cbb 65 car} } @article{chieturn88, author="Chierchia, G. and Turner, R.", title="Semantics and property theory", journal="Linguistics and Philosophy", volume="11", pages="261--302", year={1988}, tue={---} } @article{chur32, author={Church, A.}, title={A set of postulates for the foundation of logic (1)}, journal={Annals of Mathematics}, year={1932}, volume={33}, pages={346--366}, tue={IN BEZIT} } @article{chur33, author={Church, A.}, title={A set of postulates for the foundation of logic (2)}, journal={Annals of Mathematics}, year={1933}, volume={34}, pages={839--864}, tue={IN BEZIT} } @article{chur40, author={Church, A.}, title={A Formulation of the Simple Theory of Types}, journal={The Journal of Symbolic Logic}, year={1940}, volume={5}, pages={56--68}, tue={IN BEZIT} } @book{chur56, author={Church, A.}, title={Introduction to Mathematical Logic}, publisher={Princeton University Press}, year={1956}, tue={wis cbk 56 chu} } @article{chur76, author={Church, A.}, title={Comparison of {R}ussell's Resolution of the Semantic Antinomies with that of {T}arski}, journal={The Journal of Symbolic Logic}, year={1976}, volume={41}, pages={747--760}, tue={IN BIBLIOTHEEK WSK} } @article{churross36, author="Church, A. and Rosser, J.B.", title={Some properties of conversion}, journal={Transactions of the American Mathematical Society}, year={1936}, volume={39}, pages={472--482}, tue={IN BEZIT} } @book{consETAL86, author={Constable et al., R.L.}, title="Implementing Mathematics with the Nuprl Proof Development System", year={1986}, publisher={Prentice-Hall}, address={New Jersey}, tue={DGR 6 IMP} } @phdthesis{coqu85, author={Coquand, T.}, title={Une th\'eorie des constructions}, year={1985}, school={Universit\'e Paris VII}, address={Th\`ese de troisi\`eme cycle}, tue={...} } @inproceedings{coqu86, author={Coquand, T.}, title={An Analysis of {G}irard's Paradox}, booktitle={Proceedings of the Symposium on Logic in Computing Science}, year={1986}, address={Cambridge, Massachusetts}, organization={IEEE}, tue={IN BEZIT} } @article{coquhuet88, author="Coquand, T. and Huet, G.", title="The Calculus of Constructions", journal="Information and Computation", year={1988}, volume={76}, pages={95--120}, tue={...} } @book{curi86, author = {Curien, P.-L.}, title = {Categorical Combinators, Sequential Algorithms, and Functional Programming}, series = {Research Notes in Theoretical Computer Science}, publisher = {Pitman}, address = {London}, year = {1986}, pages = {xviii+300}, isbn = {0-273-08722-3}, comments = {available in U.S. from John Wiley and Sons}, checked = {7 November 1990} } @article{couscurimaun87, author = {G.~Cousineau and P.-L.~Curien and M.~Mauny}, title = {The categorical abstract machine}, journal = {Science of Computer Programming}, volume = {8(2)}, pages = {173--202}, year = {1987} } @article{curi86a, title = {Categorical Combinators}, author = {P.-L. Curien}, pages = {188--254}, journal = {Information and Control}, month = {apr / may / jun}, year = {1986}, volume = {69}, number = {1--3} } @article{curr29, author={Curry, Haskell B.}, year={1929}, title={An Analysis of Logical Substitution}, journal={American Journal of Mathematics}, volume={51}, pages={363--384}, tue={IN BEZIT} } @article{curr30, author={Curry, Haskell B.}, year={1930}, title={Grundlagen der kombinatorischen {L}ogik}, journal={American Journal of Mathematics}, volume={52}, pages={509--536, 789--834}, note={German}, tue={IN BEZIT} } @article{curr34, author={Curry, H.B.}, year={1934}, title={Functionality in combinatory logic}, journal={Proceedings of the National Academy of Science of the USA}, volume={20}, pages={584--590}, tue={IN BEZIT} } @book{curr63, author={Curry, H.B.}, year={1963}, title={Foundations of Mathematical Logic}, publisher={McGraw-Hill Book Company, Inc.}, series={McGraw-Hill Series in Higher Mathematics}, tue={wis cbk 63 cur} } @book{currfeys58, author="Curry, Haskell B. and Feys, R.", year={1958}, title={Combinatory Logic}, publisher={North-Holland}, address={Amsterdam}, volume={I}, series={Studies in Logic and the Foundations of Mathematics}, tue={wis cbk 58 cur} } @book{currhindseld72, author="Curry, H.B. and Hindley, J.R. and Seldin, J.P.", year={1972}, title={Combinatory Logic}, publisher={North-Holland}, address={Amsterdam}, volume={II}, series={Studies in Logic and the Foundations of Mathematics}, tue={wis cbk 72 cur} } %DDDD @inproceedings{daal73, author="Daalen, D.T. van", title="A description of {A}utomath and some aspects of its language theory", editor="Braffort, P.", booktitle="Proceedings of the Symposium APLASM", year="1973", volume="I", note="Also in \cite{nedegeuvvrij94}", tue={IN BEZIT} } @phdthesis{daal80, author={Daalen, D.T. van}, title="The Language Theory of Automath", year="1980", school="Eindhoven University of Technology", tue="wis cbk 80 daa" } @book{dale78, author={Dalen, D. van}, title={Filosofische grondslagen van de wiskunde}, publisher={Van Gorcum}, year={1978}, address={Assen, Amsterdam}, note={Dutch}, tue={IN BEZIT} } @book{dale81, editor={Dalen, D. van}, title={Over de Grondslagen der Wiskunde}, publisher={Mathematisch Centrum}, year={1981}, address={Amsterdam}, note={Dutch; L.E.J. Brouwers' Thesis together with unpublished fragment s, correspondence with D.J. Korteweg, review by G. Mannoury, and an introduction}, tue={cbb 81 bro} } @article{dalefreukrol81, author="Dalen, D. van and Freudenthal, H. and Krol, G.", title={De wiskundige {B}rouwer en de eenzaamheid van het gelijk}, journal={Vrij Nederland}, year={1981}, month={feb}, note={Dutch}, tue={caz 81 dal} } @techreport{damsgrumgert94, author="Dams, D. and Grumberg, O. and Gerth, R.", title={Abstract Interpretation of Reactive Systems: Abstractions Preser ving $\al$CTL*, $\er$CTL* and CTL*}, year={1994}, number={24}, institution={TUE Computing Science Notes}, address={Eindhoven University of Technology}, tue={IN BEZIT} } @article{davi73, author={Davis, M.}, title={Hilbert's tenth problem is unsolvable}, journal={American Mathematical Monthly}, volume=80, year=1973, pages={233--269} } @book{dede72, author="Dedekind, R.", title={Stetigkeit und irrationale Zahlen}, address={Braunschweig}, year={1872}, publisher={\mbox{}}, tue={...} } @article {dekk88, AUTHOR = {Dekkers, Wil}, TITLE = {Reducibility of types in typed lambda calculus. {C}omment on: ``{O}n the existence of closed terms in the typed $\lambda$-calculus, {I}'' (\ncite{stat80})}, JOURNAL = {Inform. and Comput.}, FJOURNAL = {Information and Computation}, VOLUME = {77}, YEAR = {1988}, NUMBER = {2}, PAGES = {131--137}, ISSN = {0890-5401}, } @unpublished{dekk93, author={Dekkers, W.}, title={Lambda calculus en herschrijfsystemen}, note={Lecture notes W7-HL, Catholic University of Nijmegen}, year={1993}, tue={IN BEZIT} } @proceedings{dezaplot95, editor="Dezani-Ciancaglini, Mariangiola and Plotkin, Gordon", title={Second International Conference on Typed Lambda Calculi and Applications, TLCA'95}, year={1995}, series={Lecture Notes in Computer Science}, number={902}, publisher={Springer Verlag}, tue={IN BEZIT}, address={Berlin} } @techreport{dose90, author={Dosen, K.}, title={A Brief Survey of Frames for the {L}ambek Calculus}, institution={Konstanzer Berichte zur Logik und Wissenschaftstheorie}, year={1990}, number={5}, tue={IN BEZIT reader categoriale grammatica} } @techreport{dowe91, author={{Dowek et al.}, G.}, title={The {C}oq {P}roof {A}ssistant {V}ersion 5.6, {U}sers {G}uide}, year={1991}, institution={INRIA}, number={134}, address={Le Chesney} } @phdthesis{draa95, author={Draanen, J.-P. van}, year={1995}, title={Models for simply typed lambda-calculi with fixed point combinators and enumerators}, school={Catholic University of Nijmegen}, tue={IN BEZIT} } @article{dyck97, author={Dyckhoff, R. and L. Pinto}, title={Permutability of proofs in intuitionistic sequent calculi}, note={To appear}, journal={Theoretical Computer Science}, year={1997}, } @article{dyck98, author={Dyckhoff, R. and L. Pinto}, title={Permutability of proofs in intuitionistic sequent calculi}, note={To appear}, journal={Theoretical Computer Science}, year={1998}, } %EEEE @misc{elbe96, author={Elbers, H.}, title={Personal communication}, year=1996 } @misc{eucl00, author={Euclid}, title={{T}he {E}lements}, howpublished={325 B.C. English translation in \cite{heat56}} } %FFFF @inproceedings{fefe78, author={Feferman, S.}, booktitle={Logic Colloquium '78}, year={1978}, editor={Boffa, M. and Dalen, D. van and McAloon, K}, title={Constructive Theories of Functions and Classes}, publisher={North Holland}, address={Amsterdam}, pages={159--224}, tue={IN BEZIT} } @article{fefe84, author={Feferman, S.}, title={Toward useful type-free theories {I}}, journal={Journal of Symbolic Logic}, volume={49}, year={1984}, pages={75--111}, tue={IN BEZIT} } @book{frae27, author={Fraenkel, A.}, title={Zehn Vorlesungen \"uber die Grundlegung der Mengenlehre}, year={1927}, publisher={B.G. Teubner}, address={Leipzig, Berlin}, series={Wissenschaft und Hypothese, Band XXXI}, note={German}, tue={ruu wis fr 01 1} } @book{frae28, author={Fraenkel, A.}, title={Einleitung in die Mengenlehre}, year={1928}, publisher={Springer Verlag}, address={Berlin}, series={Die Grundlehren der mathematischen Wissenschaften in Einzeldars tellungen mit besonderer Ber\"ucksichtigung der Anwendungsgebiete, Band IX}, edition={third}, note={German}, tue={ruu wis fr 01 2a} } @book{fraebarhlevy73, author="Fraenkel, A.A. and Bar-Hillel, Y. and Levy, A.", title={Foundations of Set Theory}, publisher={North Nolland}, year={1973}, series={Studies in Logic and the Foundations of Mathematics 67}, address={Amsterdam}, edition={second}, tue={wks cbf 58 fra} } @book{freg79, author={Frege, G.}, title={Begriffschrift, eine der arithmetischen nachgebildete Formelspra che des reinen Denkens}, publisher={Nebert}, address={Halle}, year={1879}, note={Also in \cite{heij67}, pages 1--82}, tue={in wis cbl 67 fro} } @book{freg84, author={Frege, G.}, title={Grundlagen der Arithmetik}, address={Breslau}, publisher={\mbox{}}, year={1884}, note={(also in \cite{benaputn83})} }