---

[Main][Contact][CV][Isabelle][Map Theory][Bibliography][Links]

Bibliography

---

Note: The following is a HTML rendering of my main bibliography file. If you find errors or omissions in the list, please let me know. If you are looking for bibliographic information for an article not in this list, you might be able to find it at CiteSeer. The HTML was generated using David Hull's bib2html converter with this style file. Information in green below is used for local purposes. Entries in dark red have not been verified, that is, only the author's name and the title of the paper is given - no attempt has been made to establish the origins of the paper.

[1]

Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Games and full abstraction for PCF: Preliminary announcement.
Lib: SCS-165.
Key: abramsky:games-full-abs-pcf.

[2]

Samson Abramsky and Guy McCusker. Game semantics. In Proceedings of Marktorberdorf '97 Summerschool, 1997. Lecture notes.
Lib: SCS-8.
Key: abramsky:game-semantics. (PostScript)

[3]

ACM. Proceedings, ACM History of Programming Languages II, April 1993.
Key: acm:hopl-ii.

[4]

Peter Aczel. An introduction to inductive definitions. In Barwise [41], chapter C.7, pages 739-782.
Lib: SCS.
Key: aczel:intro-ind-def.

[5]

Peter Aczel. Frege structures and the notions of proposition, truth and set. In The Kleene Symposium, volume 101 of Studies in Logic and the Foundations of Mathematics, pages 31-59. North-Holland, 1980.
Lib: SCS-227.
Key: aczel:frege-struct.

[6]

Sten Agerholm. A HOL Basis for Reasoning about Functional Programs. PhD thesis, University of Aarhus, December 1994. BRICS Technical Report RS-94-44.
Lib: SCS.
Key: agerholm:hol-func-prog. (PostScript)

[7]

Alfred V. Aho, Ravi Sethi, and Jeffrey D. Ullman. Compilers: Principles, Techniques, and Tools. Addison-Wesley series in Computer Science. Addison-Wesley, 1986.
Lib: SCS.
Key: aho:compilers.

[8]

Frances E. Allen. A basis for program optimization. In Freiman [129], pages 385-390.
Lib: SCS-208.
Key: allen:basis-prog-opt.

[9]

Simon J. Ambler and Roy L. Crole. Mechanized operational semantics via (co)induction. Technical Report 1998/22, Department of Mathematics and Computer Science, University of Leicester, 1998. Submitted for publication.
Lib: SCS-67.
Key: ambler:mech-op-sem. (PostScript)

[10]

Dan S. Andersen, Lars H. Pedersen, and Hans Hüttel. Objects, types and modal logics.
Lib: SCS-87.
Key: andersen:obj-typ-mod.

[11]

Lars Ole Andersen. Correctness proof for a self-interpreter. DIKU technical report, DIKU, Department of Computer Science, University of Copenhagen, December 1991.
Lib: SCS-14.
Key: andersen:correct-selfint.

[12]

Lars Ole Andersen. C program specialization. Master's thesis, DIKU, Department of Computer Science, University of Copenhagen, 1992. DIKU Technical Report 92/14.
Lib: SCS.
Key: andersen:c-spec. (PostScript) (DVI)

[13]

Nils Andersen. Approximating term rewriting systems with tree grammars. DIKU Technical Report 86/16, DIKU, Department of Computer Science, University of Copenhagen, 1986.
Lib: SCS.
Key: andersen:approx-trs.

[14]

Nils Andersen, Fritz Henglein, Neil Jones, and Torben Mogensen. Topics in lambda calculus.
Lib: SCS-123.
Key: andersen:topics-lambda.

[15]

Steen Andersen and Kim Michael Mortensen. Illative combinatory logic. Student project, DIKU, February 1999.
Lib: SCS-131.
Key: andersen:illative-comb-logic.

[16]

Peter B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Computer Science and Applied Mathematics Series. Academic Press, 1986.
Lib: DIKU.
Key: andrews:intro-ml-tt.

[17]

Andrew W. Appel. Modern Compiler Implementation in ML. Cambridge University Press, 1998.
Lib: SCS.
Key: appel:modern-comp-ml.

[18]

Kenneth Appel and Wolfgang Haken. The solution of the four-color-map problem. Scientific American, 237:108-121, October 1977.
Lib: SCS-218.
Key: appel:four-color.

[19]

Zena M. Ariola and Stefan Blom. Cyclic lambda calculi. In Martín Abadi and Takayasu Ito, editors, Theoretical Aspects of Computer Software, volume 1281 of Lecture Notes in Computer Science, pages 77-106. Springer-Verlag, 1997.
Lib: SCS-214.
Key: ariola:cyclic-lambda.

[20]

Zena M. Ariola, Matthias Felleisen, John Maraist, Martin Odersky, and Philip Wadler. A call-by-need lambda calculus. In Proceedings of POPL '95, pages 233-246. ACM Press, 1995.
Lib: SCS-98.
Key: ariola:need-lambda. (PostScript)

[21]

Ken Arnold and James Gosling. The Java Programming Language. The Java Series. Addison-Wesley, 1996.
Lib: SCS.
Key: arnold:java.

[22]

Thomas Henricus Johannes Joseph Arts. Automatically proving termination and innermost normalisation of term rewriting systems. PhD thesis, Utrecht University, May 1997.
Lib: SCS.
Key: arts:phd.

[23]

Edward Ashcroft and Zohar Manna. The translation of `go to' programs to `while' programs. In Freiman [129], pages 250-255.
Lib: SCS-203.
Key: ashcroft:goto-2-while.

[24]

Robert L. Ashenhurst and Susan Graham, editors. ACM Turing Award Lecutres: The First Twenty Years. ACM Press Anthology Series. Addison-Wesley, 1987.
Lib: SCS.
Key: acm:turing-awards.

[25]

Andrea Asperti and Giuseppe Longo. Categories, Types, and Structures: An Introduction to Category Theory for the Working Computer Scientist. Foundations of Computing. MIT Press, 1991.
Lib: SCS.
Key: asperti:cat-types-struct. (PostScript)

[26]

Lennart Augustsson. Partial evaluation in aircraft crew planning. In Hatcliff et al. [191], pages 29-40.
Lib: SCS.
Key: augustsson:aircraft-crew.

[27]

Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
Lib: SCS.
Key: baader:term-rewriting.

[28]

Brenda S. Baker. An algorithm for structuring flowgraphs. Journal of the ACM, 24(1):98-120, January 1977.
Lib: SCS-169.
Key: baker:algo-struct-fc.

[29]

Anindya Banerjee and David A. Schmidt. A categorical interpretation of Landin's correspondence principle.
Lib: SCS-166.
Key: banerjee:cat-interp-corr-prin.

[30]

Henk Barendregt. Advanced lambda calculus. Course notes.
Lib: SCS-138.
Key: barendregt:adv-lambda-calc.

[31]

H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, revised edition, 1984.
Lib: SCS.
Key: barendregt:lambda.

[32]

Henk Barendregt. Self-interpretation in lambda calculus. Journal of Functional Programming, 1(2):229-234, April 1991.
Lib: SCS-102.
Key: barendregt:selfint.

[33]

Henk Barendregt. Enumerators of lambda terms are reducing. Journal of Functional Programming, 2(2):233-236, April 1992.
Lib: SCS-190.
Key: barendregt:enum-lambda-red.

[34]

Henk Barendregt. Representing `undefined' in lambda calculus. Journal of Functional Programming, 2(3):367-374, July 1992.
Lib: SCS-189.
Key: barendregt:undef-lambda.

[35]

Henk Barendregt. Discriminating coded lambda terms, 1994.
Lib: SCS-104.
Key: barendregt:discr-lambda. (PostScript)

[36]

Henk Barendregt. The quest for correctness, April 1996.
Lib: SCS-188.
Key: barendregt:quest-correctness. (PostScript)

[37]

Henk Barendregt. The impact of the lambda calculus in logic and computer science. The Bulletin of Symbolic Logic, 3(2):181-215, June 1997.
Lib: SCS-95.
Key: barendregt:impact-lambda. (PostScript)

[38]

Henk Barendregt. Problems in type theory, February 1998.
Lib: SCS-88.
Key: barendregt:problems-type-theory. (PostScript)

[39]

Henk Barendregt and Silvia Ghilezan. Lambda terms for natural deduction, sequent calculus and cut elimination, May 1998.
Lib: SCS-100.
Key: barendregt:lambda-nat-seq-cut. (PostScript)

[40]

Michael Barr and Charles Wells. Category Theory for Computing Science. International Series in Computer Science. Prentice-Hall International, 1990.
Lib: SCS.
Key: barr:category-cs.

[41]

Jon Barwise, editor. Handbook of Mathematical Logic, volume 90 of Studies in Logic and the Foundations of Mathematics. North-Holland, 1977.
Lib: SCS.
Key: barwise:math-logic.

[42]

Michael J. Beeson. Foundations of Constructive Mathematics: Metamathematical Studies, volume 3 of Ergebnisse der Mathematik und ihrer Grenzgebeite, 3. Folge: A Series of Modern Surveys in Mathematics. Springer-Verlag, 1985.
Lib: DIKU.
Key: beeson:found-constr-math.

[43]

M. de Berg, M. van Kreveld, M. Overmars, and O. Schwarzkopf. Computational Geometry: Algorithms and Applications. Springer-Verlag, 1997.
Lib: SCS.
Key: deberg:comp-geo.

[44]

Chantal Berline and Klaus Grue. A kappa -denotional semantics for map theory in ZFC+SI. Theoretical Computer Science, 179(1-2):137-202, June 1997. DIKU Technical Report 96/11.
Lib: SCS.
Key: berline:sem-map-theory. (PostScript) (DVI)

[45]

Paul Bernays. Axiomatic Set Theory. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, second edition, 1968. Republished by Dover in 1991.
Lib: SCS.
Key: bernays:axiom-set-theory.

[46]

N. H. Bingham. Fluctuations. The Mathematical Scientist, 23:63-73, 1998.
Lib: SCS-220.
Key: bingham:fluctuations.

[47]

Richard J. Bird and Philip Wadler. Introduction to Functional Programming. International Series in Computer Science. Prentice-Hall International, 1988.
Lib: SCS.
Key: bird:func-prog.

[48]

Lars Birkedal and Morten Welinder. Partial evaluation of Standard ML. Master's thesis, DIKU, Department of Computer Science, University of Copenhagen, October 1993. DIKU Technical Report 93/22.
Lib: SCS.
Key: birkedal:sml-pe. (DVI)

[49]

Lars Birkedal and Morten Welinder. Hand-writing program generator generators. In M. Hermenegildo and J. Penjam, editors, Programming Language Implementation and Logic Programming, volume 844 of Lecture Notes in Computer Science, pages 198-214. Springer-Verlag, 1994.
Lib: SCS-148.
Key: birkedal:hand-write-pgg. (DVI)

[50]

Errett Bishop and Douglas Bridges. Constructive Analysis, volume 279 of Grundlehren der mathematischen Wissenschaften: A Series of Comprehensive Studies in Mathematics. Springer-Verlag, 1985.
Lib: DNLB.
Key: bishop:constr-anal.

[51]

Dines Bjørner, Manfred Broy, and Igor V. Pottosin, editors. Perspectives of System Informatics, volume 1181 of Lecture Notes in Computer Science. Springer-Verlag, 1996.
Lib: DIKU.
Key: sv:perspectives.

[52]

Dines Bjørner, Andrei P. Ershov, and Neil D. Jones, editors. Partial Evaluation and Mixed Computation. North-Holland, 1988.
Lib: NDJ.
Key: pe-mix:ifip-87.

[53]

James F. Blinn. A generalization of algebraic surface drawing.
Lib: SCS-47.
Key: blinn:general-alg-surf.

[54]

Jules Bloomenthal. An implicit surface polygonizer.
Lib: SCS-48.
Key: bloomenthal:impl-surf-poly.

[55]

Corrado Böhm and Alessandro Berarducci. Automatic synthesis of typed lambda -programs on term algebras. Theoretical Computer Science, 39(2-3):135-154, August 1985.
Lib: SCS-55.
Key: bohm:auto-synt.

[56]

Corrado Böhm and Alessandro Berarducci. A self-interpreter of lambda calculus having a normal form. In E. Borger, G. Jager, H. Kleine Buning, Simone Martini, and M. M. Richter, editors, Computer Science Logic, volume 702 of Lecture Notes in Computer Science, pages 85-99. Springer-Verlag, 1993.
Lib: SCS-97.
Key: bohm:norm-selfint.

[57]

Corrado Böhm and Giuseppe Jacopini. Flow diagrams, Turing machines and languages with only two formation rules. Communications of the ACM, 9(5):366-371, May 1966.
Lib: SCS-172.
Key: bohm:fd-turing-two.

[58]

Corrado Böhm, Adolfo Piperno, and Stefano Guerrini. lambda -definition of function(al)s by normal forms. In Donald Sannella, editor, Programming Languages and Systems, volume 788 of Lecture Notes in Computer Science, pages 135-149. Springer-Verlag, 1994.
Lib: SCS-54.
Key: bohm:norm-func.

[59]

Don Bolinger and Tan Bronson. Applying RCS and SCCS. O'Reilly & Associates, 1995.
Lib: SCS.
Key: bolinger:rcs-sccs.

[60]

Béla Bollobás. Modern Graph Theory, volume 184 of Graduate Texts in Mathematics. Springer-Verlag, 1998.
Lib: SCS.
Key: bollobas:modern-graph.

[61]

Anders Bondorf. Improving binding times without explicit CPS-conversion.
Lib: SCS-167.
Key: bondorf:imp-bta-wo-cps.

[62]

Anders Bondorf. Self-Applicable Partial Evaluation. PhD thesis, University of Copenhagen, 1990. DIKU Technical Report 90/17.
Lib: SCS.
Key: bondorf:self-app-pe.

[63]

Anders Bondorf. Similix manual (system version 3.0). DIKU Technical Report 91/9, DIKU, Department of Computer Science, University of Copenhagen, 1991.
Lib: SCS.
Key: bondorf:sim-man.

[64]

Anders Bondorf. Similix 5.0 Manual. DIKU, Department of Computer Science, University of Copenhagen, May 1993.
Lib: SCS-17.
Key: bondorf:similix-50.

[65]

Anders Bondorf and Olivier Danvy. Automatic autoprojection of recursive equations with global variables and abstract data types. DIKU Technical Report 90/4, DIKU, Department of Computer Science, University of Copenhagen, 1990.
Lib: SCS.
Key: bondorf:auto-auto.

[66]

François Bourdoncle. Interprocedural abstract interpretation of block structured languages with nested procedures, aliasing and recursivity.
Lib: SCS-151.
Key: bourdoncle:int-abs-int-block.

[67]

Carl B. Boyer and Uta C. Merzbach. A History of Mathematics. John Wiley & Sons, second edition, 1989.
Lib: SCS.
Key: boyer:history-math.

[68]

Ivan Bratko. Prolog: Programming for Artificial Initelligence. International Computer Science Series. Addison-Wesley, second edition, 1990.
Lib: SCS.
Key: bratko:prolog.

[69]

N. G. de Bruijn. Lambda-calculus notation with nameless dummies: a tool for automatic formula manipulation with application to the Church-Rosser theorem. Indagationes Mathematicae, 34(5):381-392, 1972. Reprinted in [294], pp. 375-388.
Lib: SCS-53.
Key: debruijn:lam-not.

[70]

N. G. de Bruijn. A survey of the project Automath. In Seldin and Hindley [379], pages 579-606. Reprinted in [294], pp. 141-161.
Lib: SCS-84.
Key: debruijn:overview-am.

[71]

Randal E. Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3):293-318, September 1992.
Key: bryant:obbd.

[72]

Victor Bryant. Aspects of Combinatorics: A wide-ranging introduction. Cambridge University Press, 1992.
Lib: SCS.
Key: bryant:aspects-comb.

[73]

Alan Bundy, Ben du Boulay, Jim Howe, and Gordon Plotkin. The researcher's bible. DAI Teaching Paper 4, Department of Artificial Intelligence, University of Edinburgh, September 1986.
Lib: SCS-111.
Key: bundy:researchers-bible.

[74]

R. M. Burstall and John Darlington. A transformation system for developing recursive programs. Journal of the ACM, 24(1):44-67, January 1977.
Lib: SCS-170.
Key: burstall:trans-sys-rec.

[75]

Luca Cardelli and Peter Wagner. On understanding types, data abstraction, and polymorphism. ACM Computing Surveys, 17(4):471-522, December 1985.
Lib: SCS-239.
Key: cardelli:understanding-types. (PDF)

[76]

Tom Cargil. C++ Programming Style. Addison-Wesley Proffesional Computing Series. Addison-Wesley, 1992.
Lib: SCS.
Key: cargill:cpp-prog-style.

[77]

Manfredo P. do Carmo. Differential Geometry of Curves and Surfaces. Prentice-Hall, 1976.
Lib: SCS.
Key: docarmo:diff-geom.

[78]

Martin Carroll. Getting a Ph.D.
Lib: SCS-112.
Key: carroll:getting-phd.

[79]

Per Cederqvist. Version Management with CVS. Signum Support AB, 1993. For CVS 1.8.1.
Lib: SCS.
Key: cederqvist:cvs.

[80]

Eugene Charniak, Christopher K. Riesbeck, and Drew V. McDermott. Artificial Intelligence Programming. Lawrence Erlbaum Associates, 1980.
Lib: TUM.
Key: charniak:ai-programming.

[81]

Bernard Chazelle. The Discrepancy Method. Cambridge University Press, 2002.
Lib: SCS.
Key: chazelle:discrepancy.

[82]

Wei-Ngan Chin and John Darlington. Removing higher-order expressions by program transformation.
Lib: SCS-152.
Key: chin:rem-ho-exp-pt.

[83]

Alonzo Church. A set of postulates for the foundation of logic. Annals of Mathematics, 33:346-366, 1932.
Lib: SCS-235.
Key: church:postulates-found-logic.

[84]

Alonzo Church. A set of postulates for the foundation of logic (second paper). Annals of Mathematics, 34:839-864, 1933.
Lib: SCS-238.
Key: church:postulates-found-logic-2.

[85]

Alonzo Church. An unsolvable problem of elementary number theory. American Journal of Mathematics, 58:345-363, 1936.
Lib: SCS-231.
Key: church:unsolvable.

[86]

Alonzo Church. A formulation of the simple theory of types. The Journal of Symbolic Logic, 5(2):56-68, June 1940.
Lib: SCS-234.
Key: church:simpl-types.

[87]

Alonzo Church and S. C. Kleene. Formal definitions in the theory of ordinal numbers. Fundamenta Mathematicae, 28:11-21, 1937.
Lib: SCS-230.
Key: church:form-def-ordinals.

[88]

Alonzo Church and J. B. Rosser. Some properties of conversion. Transactions of the American Mathematical Society, 39:472-482, 1936.
Lib: SCS-219.
Key: church:prop-conv.

[89]

Cristina Cifuentes. Reverse Compilation Techniques. PhD thesis, Queensland University of Technology, July 1994.
Lib: SCS-200.
Key: cifuentes:rev-comp-tech. (DVI)

[90]

Cristina Cifuentes. Struturing decompiled graphs. In Tibor Gyimóthy, editor, Compiler Construction, volume 1060 of Lecture Notes in Computer Science, pages 91-105. Springer-Verlag, 1996.
Lib: SCS-209.
Key: cifuentes:struct-dec-graph.

[91]

John Cocke. Global common subexpression elimination. ACM SIGPLAN Notices, 5(7):20-24, July 1970.
Lib: SCS-207.
Key: cocke:glob-com-subexp-elim.

[92]

Charles Consel. Report on Schism, January 1996.
Lib: SCS.
Key: consel:rep-schism.

[93]

David C. Cooper. Böhm and Jacopini's reduction of flow charts. Communications of the ACM, 10(8):463, 473, August 1967.
Lib: SCS-201.
Key: cooper:bj-answer.

[94]

Thierry Coquand and Gérard Huet. The calculus of constructions. Information and Computation, 76(2/3):95-120, February/March 1988.
Lib: SCS-204.
Key: coquand:coc.

[95]

Loïc Correnson, Etienne Duris, Didier Parigot, and Gilles Roussel. Generic programming by program composition (position paper).
Lib: SCS-186.
Key: correnson:gen-pr-pc.

[96]

Roy L. Crole. Categories for Types. Cambridge University Press, 1993.
Lib: SCS.
Key: crole:categories.

[97]

David A. Curry. Using C on the UNIX System. O'Reilly & Associates, 1989.
Lib: SCS.
Key: curry:c-unix.

[98]

Dirk van Dalen. Logic and Structure. Universitext. Springer-Verlag, third augmented edition, 1994.
Lib: DIKU.
Key: vandalen:logic-struct.

[99]

Luis Damas and Robin Milner. Principal type-schemes for functional programs. In 9th ACM Symposium on Principles of Programming Languages, pages 207-212. ACM Press, 1982.
Lib: SCS-121.
Key: damas:prin-ts-fp.

[100]

Flemming M. Damm. Subtyping with union types, intersection types and recursive types. In M. Hagiya and John C. Mitchell, editors, Theoretical Aspects of Computer Software, volume 789 of Lecture Notes in Computer Science, pages 687-706. Springer-Verlag, 1994.
Lib: SCS-122.
Key: damm:subt.

[101]

Olivier Danvy. Some advice on giving a talk. Slides.
Lib: SCS-178.
Key: danvy:advice-talk. (PostScript) (PDF) (DVI)

[102]

Olivier Danvy. Memory allocation and higher-order functions: Capture, sharing, and incremental recovery, an alternative to the stack strategy using a heap memory. DIKU Technical Report 87/1, DIKU, Department of Computer Science, University of Copenhagen, 1987.
Lib: SCS.
Key: danvy:mem-alloc.

[103]

Olivier Danvy and Andrzej Filinski. A functional abstraction of typed contexts. DIKU Technical Report 89/12, DIKU, Department of Computer Science, University of Copenhagen, 1989.
Lib: SCS.
Key: danvy:func-abs-typ-cont.

[104]

Olivier Danvy, Robert Glück, and Peter Thiemann, editors. Partial Evaluation, volume 1110 of Lecture Notes in Computer Science. Springer-Verlag, 1996.
Lib: DIKU.
Key: lncs:1110.

[105]

Olivier Danvy, Karoline Malmkjær, and Jens Palsberg. The essence of eta-expansion in partial evaluation. LISP and Symbolic Computation, 8(3):209-227, 1995.
Lib: SCS-163.
Key: danvy:essence-eta-exp. (PostScript)

[106]

Olivier Danvy and Morten Rhiger. Compiling actions by partial evaluation, revisited. Technical Report RS-98-13, BRICS, Department of Computer Science, University of Aarhus, 1998.
Lib: SCS-28.
Key: danvy:comp-act-pe. (PostScript) (PDF) (DVI)

[107]

Richard Dedekind. Essays on the Theory of Numbers. The Open Court Publishing Company, 1901. Translations of Stetigkeit und irrationale Zahlen and Was sind und was sollen die Zahlen by Wooster Woodruff Beman. Republished by Dover in 1963.
Lib: SCS.
Key: dedekind:numbers.

[108]

Richard A. DeMillo, Richard J. Lipton, and Alan J. Perlis. Social processes and proofs of theorems and programs. Communications of the ACM, 22(5):271-280, May 1979.
Lib: SCS-109.
Key: demillo:social-process.

[109]

Joëlle Despeyroux. Proof of translation in natural semantics, July 1987.
Lib: SCS-16.
Key: despeyroux:proof-trans.

[110]

Keith Devlin. Sets, Functions and Logic: An introduction to abstract mathematics. Chapman & Hall Mathematics. Chapman & Hall, second edition, 1992.
Lib: SCS.
Key: devlin:set-func-logic.

[111]

Edsger W. Dijkstra. Go to statement considered harmful. Communications of the ACM, 11(3):147-148, March 1968.
Lib: SCS-171.
Key: dijkstra:goto-harmful.

[112]

Dale Dougherty. sed & awk. O'Reilly & Associates, 1990.
Lib: SCS.
Key: dougherty:sed-awk.

[113]

Lyn Dupré. Bugs in Writing: A Guide to Debugging Your Prose. Addison-Wesley, revised edition, 1998.
Lib: SCS.
Key: dupre:bugs-writing.

[114]

Peter Dybjer. Inductive families.
Lib: SCS-225.
Key: dybjer:inductive-families.

[115]

Peter Dybjer and Anton Setzer. A finite axiomatization of inductive-recursive definitions.
Lib: SCS-226.
Key: dybjer:finite-ax-ir-def.

[116]

Hans Dybkjær. Category Theory, Types, and Programming Languages. PhD thesis, University of Copenhagen, March 1991. DIKU Technical Report 91/11.
Lib: SCS.
Key: dybkjaer:cat-theory.

[117]

R. Kent Dybvig. The Scheme Programming Language. Prentice-Hall, 1987.
Lib: DIKU.
Key: dybvig:scheme.

[118]

R. Kent Dybvig. The Scheme Programming Language. Prentice-Hall, second edition, 1996.
Key: dybvig:scheme-2nd.

[119]

Belmina Dzafic. Formalizing program transformations. Master's thesis, DAIMI, Department of Computer Science, University of Aarhus, December 1998.
Lib: SCS-128.
Key: dzafic:form-prog-trans.

[120]

Martin Elsman. Optimising typed programs. Course notes, 1998.
Lib: SCS.
Key: elsman:otp.

[121]

Ana M. Erosa and Laurie J. Hendren. Taming control flow: A structured approach to eliminating goto statements. In Proceedings of the 1994 International Conference on Computer Languages [211], pages 229-240.
Lib: SCS-56.
Key: erosa:taming-goto. (PostScript)

[122]

Faculty of Mathematics and Computer Science, University of Nijmegen. Summer School in Lambda Calculus, Nijmegen, The Netherlands, July 1991.
Lib: SCS-144.
Key: lambda:nijmegen.

[123]

Jay Fenlason and Richard Stallman. GNU gprof. Free Software Foundation, 1998.
Lib: SCS-210.
Key: fenlason:gprof.

[124]

Adrian Fiech. Category of Delta -functors.
Lib: SCS-168.
Key: fiech:cat-delta-func.

[125]

Andrzej Filinski. Declarative continuations and categorical duality. Master's thesis, DIKU, Department of Computer Science, University of Copenhagen, July 1989. DIKU Technical Report 89/11.
Lib: SCS.
Key: filinski:decl-cont-cat-dual.

[126]

Andrzej Filinski. From normalization by evaluation to type-directed partial evaluation, May 1998. Slides.
Lib: SCS-143.
Key: filinski:norm-eval-td-pe.

[127]

Melvin Fitting. First-Order Logic and Automated Theorem Proving. Graduate Texts in Computer Science. Springer-Verlag, second edition, 1996.
Lib: DIKU.
Key: fitting:fo-logic-atp.

[128]

James D. Foley, Andries van Dam, Steven K. Feiner, and John F. Hughes. Computer Graphics: Principles and Practice. Addison-Wesley System Programming Series. Addison-Wesley, second in c edition, 1996.
Lib: SCS.
Key: vandam:computer-graphics.

[129]

C. V. Freiman, editor. Information Processing 71, volume 1. North-Holland, 1972.
Lib: DIKU.
Key: ifip:71.

[130]

Jacob Frost. A case study of co-induction in Isabelle. Technical Report 359, University of Cambridge, Computer Laboratory, February 1995.
Lib: SCS-66.
Key: frost:coind-isa. (DVI)

[131]

You-Chin Fuh and Prateek Mishra. Polymorphic subtype inference: Closing the theory-practice gap. In Josep Díaz and Fernando Orejas, editors, TAPSOFT '89, volume 352 of Lecture Notes in Computer Science. Springer-Verlag, 1989.
Lib: SCS-116.
Key: fuh:poly-sub-inf.

[132]

You-Chin Fuh and Prateek Mishra. Type inference with subtypes. Theoretical Computer Science, 73(2):155-175, June 1990.
Lib: SCS-115.
Key: fuh:type-inf-subtypes.

[133]

Yoshihiko Futamura. Partial evaluation of computing process--an approach to a compiler-compiler. Systems, Computers, Controls, 2(5):45-50, 1971.
Lib: SCS-25.
Key: futamura:pe.

[134]

Yoshihiko Futamura. Partial computation of programs. In Eiichi Goto, Koichi Furukawa, Reiji Nakajima, Ikuo Nakata, and Akinori Yonezawa, editors, RIMS Symposia on Software Science and Engineering, volume 147 of Lecture Notes in Computer Science, pages 1-35. Springer-Verlag, 1983.
Lib: SCS-26.
Key: futamura:pe-prog.

[135]

Yoshihiko Futamura and Kenroku Nogi. Generalized partial computation. In Bjørner et al. [52], pages 133-151.
Lib: SCS-22.
Key: futamura:gen-pc.

[136]

Murdoch Gabbay and Andrew Pitts. A new approach to abstract syntax involving binders. In 14th Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, 1999. To appear.
Lib: SCS-193.
Key: gabbay:new-approach. (PostScript) (PDF)

[137]

Gerald C. Gannod and Betty H. C. Chang. Using informal and formal. In Proceedings of the 1996 IEEE International Conference on Software Maintenance, pages 265-274. IEEE Computer Society Press, November 1996.
Key: gannod:inf-form-rev-c. (PostScript)

[138]

Simson Garfinkel and Gene Spafford. Practical UNIX Security. O'Reilly & Associates, 1991.
Lib: SCS.
Key: garfinkel:unix-sec.

[139]

N. D. Gilbert and T. Porter. Knots and Surfaces. Oxford University Press, 1994.
Lib: SCS.
Key: gilbert:knots-surf.

[140]

Robert Gilmore. Catastrophe Theory for Scientists and Engineers. John Wiley & Sons, New York, 1981. Republished by Dover in 1993.
Lib: SCS.
Key: gilmore:catastrophe-theory.

[141]

Robert Glück. On the generation of specializers. Journal of Functional Programming, 4(4):499-514, October 1994.
Lib: SCS-42.
Key: glueck:gen-spec.

[142]

Robert Glück. On the mechanics of metasystem hierarchies in program transformation. In M. Proietti, editor, Logic Program Synthesis and Transformation, volume 1048 of Lecture Notes in Computer Science, pages 234-251. Springer-Verlag, 1996.
Lib: SCS-149.
Key: glueck:mech-meta-hier.

[143]

Robert Glück and Neil D. Jones. Automatic program specialization by partial evaluation: an introduction. In W. Mackens and S. M. Rump, editors, Software Engineering im Scientific Computing, pages 70-77. Vieweg, 1996.
Lib: SCS-185.
Key: glueck:aps-pe. (PostScript)

[144]

Robert Glück and Jesper Jørgensen. Generating transformers for deforestation and supercompilation of higher-order languages. Outline.
Lib: SCS-175.
Key: glueck:gen-trans-ho.

[145]

Robert Glück and Jesper Jørgensen. Generating optimizing specializers. In Proceedings of the 1994 International Conference on Computer Languages [211].
Lib: SCS-20.
Key: glueck:gen-opt-spec. (DVI)

[146]

Robert Glück and Jesper Jørgensen. Generating transformers for deforestation and supercompilation. In B. Le Charlier, editor, Static Analysis, volume 864 of Lecture Notes in Computer Science, pages 432-448. Springer-Verlag, 1994.
Lib: SCS-21.
Key: glueck:gen-trans. (DVI)

[147]

Robert Glück and Jesper Jørgensen. Efficient multi-level generating extensions for program specialization. In Hermenegildo and Doaitse Swierstra [200], pages 259-278.
Lib: SCS-150.
Key: glueck:eff-multi-lvl-ge. (PostScript)

[148]

Robert Glück and Jesper Jørgensen. Fast binding-time analysis for multi-level specialization. In Bjørner et al. [51], pages 261-272.
Lib: SCS-37.
Key: glueck:fast-binding-mls.

[149]

Robert Glück and Jesper Jørgensen. An automatic program generator for multi-level specialization. LISP and Symbolic Computation, 10(2):113-158, 1997.
Lib: SCS-43.
Key: glueck:apg-mls.

[150]

Robert Glück and Jesper Jørgensen. Multi-level specialization (extended abstract). In Hatcliff et al. [191], pages 69-81.
Lib: SCS.
Key: glueck:multi-level-spec.

[151]

Robert Glück and Andrei V. Klimov. Occam's razor in metacomputation: the notion of a perfect process tree. In P. Cousot, M. Falaschi, G. Filè, and A. Rauzy, editors, 3rd International Workshop on Static Analysis, volume 724 of Lecture Notes in Computer Science, pages 112-123. Springer-Verlag, 1993.
Lib: SCS-18.
Key: glueck:occam. (PostScript)

[152]

Robert Glück and Andrei Klimov. On the degeneration of program generators by program composition. New Generation Computing, 16(1):75-95, 1998.
Lib: SCS-36.
Key: glueck:deg-prog-gen.

[153]

Robert Glück and Morten Heine Sørensen. A roadmap to metacomputation by supercompilation, 1996.
Lib: SCS-164.
Key: glueck:roadmap-metac-superc. (PostScript)

[154]

Kurt Gödel. Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Mathematik und Physik, 38:173-198, 1931.
Lib: SCS-232.
Key: godel:undecidable-prin-math.

[155]

J. A. Goguen, J. W. Thatcher, and E. G. Wagner. An initial algebra approach to the specification, correctness, and implementation of abstract data types. In Raymond T. Yeh, editor, Data Structuring, volume 4 of Current Trends in Programming Methodology, chapter 5, pages 80-149. Prentice-Hall, 1978.
Lib: SCS-10.
Key: goguen:int-alg.

[156]

Carsten K. Gomard. Higher Order Partial Evaluation---HOPE for the lambda calculus. Master's thesis, DIKU, Department of Computer Science, University of Copenhagen, September 1989.
Lib: SCS-129.
Key: gomard:hope-lambda.

[157]

Carsten K. Gomard. Partial type inference for untyped functional programs. In Proceedings of the 1990 ACM Conference on Lisp and Functional Programming, pages 282-287, Nice, France, June 1990. ACM Press. Extended abstract.
Lib: SCS-114.
Key: gomard:part-type-inf.

[158]

Carsten Krogh Gomard. Program Analysis Matters. PhD thesis, University of Copenhagen, November 1991. DIKU Technical Report 91/17.
Lib: SCS.
Key: gomard:prog-anal.

[159]

Carsten K. Gomard. A self-applicable partial evaluator for the lambda calculus: Correctness and pragmatics. ACM Transactions on Programming Languages and Systems, 14(2):147-172, April 1992.
Lib: SCS-44.
Key: gomard:toplas. (PDF)

[160]

Carsten K. Gomard and Neil D. Jones. Compiler generation by partial evaluation: a case study. Structured Programming, 12:123-144, 1991. DIKU Technical Report 90/16.
Lib: SCS.
Key: gomard:comp-gen-pe.

[161]

Carsten K. Gomard and Neil D. Jones. A partial evaluator for the untyped lambda-calculus. Journal of Functional Programming, 1(1):21-69, January 1991.
Lib: SCS-27.
Key: gomard:pe-unt-lambda.

[162]

Richard Goodman, editor. Annual Review in Automatic Programming, volume 1. Pergamon Press, 1960.
Lib: DIKU.
Key: annreview:1.

[163]

Michel Goossens, Frank Mittelbach, and Alexander Samarin. The LaTeX Companion. Addison-Wesley, 1994.
Lib: SCS.
Key: goossens:latex-companion.

[164]

Michel Goossens, Sebastian Rahtz, and Frank Mittelbach. The LaTeX Graphics Companion: Illustrating documents with TeX and PostScript. Addison-Wesley, 1997.
Lib: SCS.
Key: goossens:latex-gfx-companion.

[165]

Michael J. C. Gordon. Mechanizing programming logics in higher order logic. In G. Birtwistle and P. A. Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem Proving, pages 387-439. Springer-Verlag, 1989.
Lib: SCS-85.
Key: gordon:mech-prog-ho. (DVI)

[166]

M. J. C. Gordon and T. F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993.
Lib: DIKU.
Key: gordon:intro-hol.

[167]

Michael Gordon, Robin Milner, and Christopher Wadsworth, editors. Edinburgh LCF: A Mechanised Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.
Lib: DIKU.
Key: gordon:edinburgh-lcf.

[168]

David Griffioen and Marieke Huisman. A comparison of PVS and Isabelle/HOL. In Grundy and Newey [176], pages 123-142.
Lib: SCS-86.
Key: griffioen:pvs-isabell-hol. (PostScript)

[169]

Klaus E. Grue. An efficient formal theory. DIKU Technical Report 87/14, DIKU, Department of Computer Science, University of Copenhagen, February 1987.
Lib: SCS.
Key: grue:eff-form-theory.

[170]

Klaus Grue. Map theory. Theoretical Computer Science, 102(1):1-133, August 1992.
Lib: SCS.
Key: grue:map-theory.

[171]

Klaus Grue. Map theory: Preface, appendix and index. DIKU Technical Report 92/16, DIKU, Department of Computer Science, University of Copenhagen, October 1992.
Lib: SCS.
Key: grue:map-pref-app-index.

[172]

Klaus Grue. Mathematics and computation. Course notes, 1994-2001.
Lib: SCS.
Key: grue:math-comp.

[173]

Klaus Grue. Stable map theory. DIKU Technical Report 96/10, DIKU, Department of Computer Science, University of Copenhagen, April 1996.
Lib: SCS.
Key: grue:stable-mt. (PostScript)

[174]

Klaus Grue. lambda -calculus as a foundation of mathematics, August 1997. To appear in the Church Memorial Volume.
Lib: SCS-177.
Key: grue:lcalc-found-math. (PostScript) (DVI)

[175]

Klaus Grue. Map theory with classical maps. As yet unpublished. Can be found from url http://www.diku.dk/users/grue, 2001.
Lib: SCS.
Key: grue:mt-classical.

[176]

J. Grundy and M. Newey, editors. Theorem Proving in Higher Order Logics, volume 1479 of Lecture Notes in Computer Science. Springer-Verlag, September 1998.
Lib: DIKU.
Key: lncs:1479.

[177]

Carl A. Gunter. Semantics of Programming Languages: Structures and Techniques. Foundations of Computing. MIT Press, 1992.
Lib: SCS.
Key: gunter:formal-semantics.

[178]

Paul R. Halmos. Naive Set Theory. The University series in undergraduate mathematics. Van Nostrand, 1960. Republished by Springer-Verlag in 1974 in the Undergraduate texts in mathematics series.
Lib: SCS.
Key: halmos:naive-set-theory.

[179]

P. R. Halmos. How to write mathematics. L'Enseignement Mathématique, 16:123-152, 1970. Reprinted in [122].
Key: halmos:how-write-math.

[180]

P. R. Halmos. How to talk mathematics. AMS NOTICES, 21(3):155-158, April 1974. Reprinted in [122].
Key: halmos:how-talk-math.

[181]

John Hannan. An introduction to classical logic as a programming language. Slides.
Lib: SCS-154.
Key: hannan:intro-clas-logic-pl.

[182]

John J. Hannan. Investigating a Proof-Theoretic Meta-Language for Functional Programs. PhD thesis, University of Pennsylvania, 1991.
Lib: SCS.
Key: hannan:doctoral.

[183]

John Hannan and Dale Miller. Uses of higher-order unification for implementing program transformers. In Robert A. Kowalski and Kenneth A. Bowen, editors, Fifth International Logic Programming Conference, pages 942-959. MIT Press, 1988.
Lib: SCS-127.
Key: hannan:ho-uni-prog-trans.

[184]

John Harrison. Constructing the real numbers in HOL. Formal Methods in System Design, 5(1-2):35-59, July 1994.
Lib: SCS-69.
Key: harrison:construct-real. (PostScript)

[185]

John Harrison. Formalized mathematics. TUCS Technical Report 36, Turku Centre for Computer Science, August 1996.
Lib: SCS-110.
Key: harrison:form-math. (PostScript) (DVI)

[186]

Ronald Harrop. Concerning formulas of the types A to B land C, A to (Ex)B(x) in intuitionistic formal systems. The Journal of Symbolic Logic, 25(1):27-32, March 1960.
Lib: SCS-222.
Key: harrop:disj-ext-intuitionistic-systems.

[187]

Juris Hartmanis. Gödel, von Neumann and the P=?NP problem.
Lib: SCS-108.
Key: hartmanis:godel-von-neumann.

[188]

John Hatcliff. Mechanically verifying the correctness of an offline partial evaluator. In Hermenegildo and Doaitse Swierstra [200], pages 279-298.
Lib: SCS.
Key: hatcliff:mech-verif-correctness. (DVI)

[189]

John Hatcliff. Mechanically verifying the correctness of an offline partial evaluator (extended version). DIKU Technical Report 95/14, DIKU, Department of Computer Science, University of Copenhagen, 1996. Revised version of [188].
Lib: SCS.
Key: hatcliff:mech-verif-correctness-ext. (PostScript)

[190]

John Hatcliff. An introduction to partial evaluation using a simple flowchart language. In Hatcliff et al. [191], pages 21-90.
Lib: SCS.
Key: hatcliff:fcl.

[191]

John Hatcliff, Torben Æ. Mogensen, and Peter Thiemann, editors. Partial Evaluation: Practice and Theory, Copenhagen, July 1998.
Lib: SCS.
Key: diku:pe-summerschool-98.

[192]

Klaus Havelund. The Fork Calculus: Towards a Logic for Concurrent ML. PhD thesis, University of Copenhagen, 1994. DIKU Technical Report 94/4.
Lib: SCS.
Key: havelund:fork-calculus.

[193]

Matthew S. Hecht and Jeffrey D. Ullman. Flow graph reducibility. SIAM Journal of Computing, 1(2):188-202, June 1972.
Lib: SCS-206.
Key: hecht:flow-graph-red.

[194]

M. S. Hecht and J. D. Ullman. Characterizations of reducible flow graphs. Journal of the ACM, 21(3):367-375, July 1974.
Lib: SCS-199.
Key: hecht:char-red-fg.

[195]

Paul S. Heckbert. Survey of texture mapping.
Lib: SCS-45.
Key: heckbert:survey-text-map.

[196]

Jean van Heijenoort. From Frege to Gödel: A source book in mathematical logic 1879-1931. Harvard University Press, 1967.
Lib: SCS.
Key: van-heijenoort:from-frege.

[197]

Fritz Henglein. Simple type inference and unification.
Lib: SCS-125.
Key: henglein:simple-ti-uni.

[198]

Fritz Henglein. Fundamentals of type inference systems. Course notes, 1994.
Lib: SCS-119.
Key: henglein:fund-type-inf-sys.

[199]

Fritz Henglein. Introduction to lambda calculus and operational semantics of functional programming languages. Course notes, 1994.
Lib: SCS-134.
Key: henglein:intro-lambda.

[200]

M. Hermenegildo and D. Doaitse Swierstra, editors. Programming Languages: Implementations, Logics and Programs, volume 982 of Lecture Notes in Computer Science. Springer-Verlag, 1995.
Lib: DIKU.
Key: lncs:982.

[201]

Steve Hill and Simon Thompson. Miranda in Isabelle. In Lawrence C. Paulson, editor, Proceedings of the First Isabelle Users Workshop, pages 122-135, September 1995.
Lib: SCS-68.
Key: hill:miranda. (PostScript)

[202]

J. Roger Hindley. Basic Simple Type Theory, volume 42 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1997.
Lib: SCS.
Key: hindley:basic-simple.

[203]

My Hoang and John C. Mitchell. Lower bounds on type inference with subtypes.
Lib: SCS-120.
Key: hoang:lower-bounds-typ-inf.

[204]

C. A. R. Hoare and D. C. S. Allison. Incomputability. ACM Computing Surveys, 4(3):169-178, September 1972.
Lib: SCS-191.
Key: hoare:incomp.

[205]

John G. Hocking and Gail S. Young. Topology. Addison-Wesley Series in Mathematics. Addison-Wesley, 1961. Republished with corrections by Dover in 1988.
Lib: SCS.
Key: hocking:topology.

[206]

Gary Hoffman and Glynis Hoffman. Adios, Strunk and White. Verve Press, second edition, 1999.
Lib: SCS.
Key: hoffman:adios-strunk-white.

[207]

W. A. Howard. The formulae-as-types notion of construction. In Seldin and Hindley [379], pages 479-490.
Lib: SCS-132.
Key: howard:formulae-as-types.

[208]

Gérard Huet. Cartesian closed categories and lambda-calculus. Notes.
Lib: SCS-9.
Key: huet:ccc-lambda.

[209]

Gérard Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the ACM, 27(4):797-821, October 1980.
Lib: SCS-228.
Key: huet:confl-red.

[210]

Gérard Huet, Gilles Kahn, and Christine Paulin-Mohring. The Coq proof assistant: A tutorial.
Lib: SCS-59.
Key: coq:tutorial.

[211]

IEEE Computer Society. Proceedings of the 1994 International Conference on Computer Languages. IEEE Computer Society Press, 1994.
Key: ieee:iccl94.

[212]

Hideya Iwasaki, Zhenjiang Hu, and Masato Takeichi. Towards manipulation of mutually recursive functions. In M. Sato and Y. Toyama, editors, Third Fuji International Symposium on Functional and Logic Programming. World Scientific, 1998.
Lib: SCS-40.
Key: iwasaki:manipulation.

[213]

C. Barry Jay. A semantics for shape. Science of Computer Programming, 25(2-3):251-283, December 1995.
Lib: SCS-184.
Key: jay:semantics-shape.

[214]

Peter Johansen, editor. Proceedings fra Den Anden Danske Konference om Mønstergenkendelse og Billedanalyse, 1993. DIKU Technical Report 93/17.
Lib: SCS.
Key: johansen:anden-dk-konf.

[215]

Peter Johansen, editor. Proceedings of the Copenhagen Workshop on Gaussian Scale-Space Theory, 1996. DIKU Technical Report 96/19.
Lib: SCS.
Key: johansen:guassian-scale-space.

[216]

Claes Johnson. Numerical solution of partial differential equations by the finite element method. Studentlitteratur, 1987.
Lib: SCS.
Key: johnson:pde-by-fem.

[217]

Neil D. Jones. Flow analysis of lazy higher-order functional languages. In S. Abramsky and C. Hankin, editors, Abstract Interpretation of Declarative Languages, pages 103-122. Ellis Horwood, 1987. DIKU Technical Report 86/15.
Lib: SCS.
Key: jones:flow-anal.

[218]

Neil D. Jones. Challenging problems in partial evaluation and mixed computation. In Bjørner et al. [52], pages 1-14.
Lib: SCS-62.
Key: jones:challenge.

[219]

Neil D. Jones. Partial evaluation and the generation of program generators. DIKU Technical Report 92/18, DIKU, Department of Computer Science, University of Copenhagen, 1992.
Lib: SCS.
Key: jones:pe-gpg. (PostScript) (DVI)

[220]

Neil D. Jones. What not to do when writing an interpreter for specialization. In Danvy et al. [104], pages 216-237.
Lib: SCS-19.
Key: jones:not-to-do. (PostScript) (DVI)

[221]

Neil D. Jones. Computability and Complexity: From a Programming Perspective. Foundations of Computing. MIT Press, 1997.
Lib: SCS.
Key: jones:comp-and-comp.

[222]

Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. Partial Evaluation and Automatic Program Generation. International Series in Computer Science. Prentice-Hall International, 1993.
Lib: SCS.
Key: jones:pe-and-apg.

[223]

Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. Partial evaluation for the lambda calculus. In Hatcliff et al. [191], pages 13-27. Abbreviated version of chapter 8 of [222].
Lib: SCS.
Key: jones:partial-lambda-calculus.

[224]

Neil D. Jones and Flemming Nielson. Abstract interpretation: A semantics-based tool for program analysis. In Handbook of Logic in Computer Science, pages 527-629. Oxford University Press, 1994. DIKU Technical Report 94/2.
Lib: SCS.
Key: jones:abs-int. (PostScript) (DVI)

[225]

Neil D. Jones, Peter Sestoft, and Harald Søndergaard. An experiment in partial evaluation: The generation of a compiler generator. DIKU Technical Report 85/1, DIKU, Department of Computer Science, University of Copenhagen, January 1985.
Lib: SCS.
Key: jones:mix-exp.

[226]

Neil D. Jones, Peter Sestoft, and Harald Søndergaard. Mix: A self-applicable partial evaluator for experiments in compiler generation. LISP and Symbolic Computation, 2(1):9-50, 1989. DIKU Technical Report 91/12, revised version of 87/8.
Lib: SCS.
Key: jones:mix-rev.

[227]

Jesper Jørgensen. Similix: A self-applicable partial evaluator for Scheme. In Hatcliff et al. [191], pages 91-115.
Lib: SCS.
Key: jorgensen:similix.

[228]

Richard Kelsey, William Clinger, and Jonathan Rees. Revised⁵ report on the algorithmic language Scheme. ACM SIGPLAN Notices, 33(9):26-76, September 1998. With H. Abelson, N. I. Adams, IV, D. H. Bartley, G. Brooks, R. K. Dybvig, D. P. Friedman, R. Halstead, C. Hanson, C. T. Haynes, E. Kohlbecker, D. Oxley, K. M. Pitman, G. J. Rozas, G. L. Steele, Jr., G. J. Sussman, and M. Wand.
Lib: SCS.
Key: kelsey:scheme5. (PostScript) (DVI)

[229]

Brian W. Kernighan and Dennis M. Ritchie. The C Programming Language. Prentice-Hall, second edition, 1988.
Lib: SCS.
Key: def:ansi-c.

[230]

David Kincaid and Ward Cheney. Numerical Analysis. Brooks/Cole Publishing Company, 1991.
Lib: SCS.
Key: kincaid:numerical-analysis.

[231]

Gary A. Kindall. A unified approach to global program optimization. In Symposium on Principles of Programming Languages, pages 194-206, October 1973.
Lib: SCS-205.
Key: kildall:uni-glob-prog-opt.

[232]

Stephen C. Kleene. Origins of recursive function theory. Annals of the History of Computing, 3(1):52-67, January 1981.
Lib: SCS-236.
Key: kleene:origins-rec-func-theory.

[233]

S. C. Kleene and J. B. Rosser. The inconsistency of certain formal logics. Annals of Mathematics, 36(3):630-636, July 1935.
Lib: SCS-229.
Key: kleene:incons-formal-logics.

[234]

Andrei V. Klimov. Program specialization vs. program composition. ACM Computing Surveys, 30(3es):3-es, September 1998.
Lib: SCS-187.
Key: klimov:ps-vs-pc. (PDF)

[235]

Jan Willem Klop. Combinatory Reduction Systems. PhD thesis, Utrecht University, Amsterdam, 1980. CWI Tract 127.
Lib: PMN.
Key: klop:thesis.

[236]

Donald E. Knuth. Fundamental Algorithms, volume 1 of The Art of Computer Programming. Addison-Wesley, second edition, 1973.
Lib: SCS.
Key: knuth:art-1.

[237]

Donald E. Knuth. Sorting and Searching, volume 3 of The Art of Computer Programming. Addison-Wesley, 1973.
Lib: SCS.
Key: knuth:art-3.

[238]

Donald E. Knuth. Structured programming with go to statements. ACM Computing Surveys, 6(4):261-302, December 1974. Reprinted as chapter 2 in [240].
Key: knuth:structure-goto.

[239]

Donald E. Knuth. Seminumerical Algorithms, volume 2 of The Art of Computer Programming. Addison-Wesley, second edition, 1981.
Lib: SCS.
Key: knuth:art-2.

[240]

Donald E. Knuth. Literate Programming. Number 27 in CSLI Lecture Notes. Center for the Study of Language and Information, 1992.
Lib: DIKU.
Key: knuth:literate.

[241]

Donald E. Knuth. The TeX book, volume A of Computers & Typesetting. Addison-Wesley, revised edition, 1992.
Lib: SCS.
Key: knuth:tex.

[242]

D. E. Knuth and R. W. Floyd. Notes on avoiding ``go to'' statements. Information Processing Letters, 1:23-31, 1971.
Lib: SCS-198.
Key: knuth:notes-goto.

[243]

Donald E. Knuth, Tracy Larrabee, and Paul M. Roberts. Mathematical Writing. Number 14 in Mathematical Association of America Notes. Mathematical Association of America, 1989. Republished by Cambridge University Press in 1996.
Lib: SCS.
Key: knuth:math-writ. (DVI)

[244]

Jan Kuper. An axiomatic theory for partial functions. Information and Computation, 107(1):104-150, November 1993.
Lib: SCS-183.
Key: kuper:axiom-part-func.

[245]

J. Kuper. Partiality in Logic and Computation--Aspects of Undefinedness. PhD thesis, University of Twente, 1994.
Lib: SCS-182.
Key: kuper:phd.

[246]

Imre Lakatos. Proofs and Refutations: The Logic of Mathematical Discovery. Cambridge University Press, 1976.
Lib: SCS.
Key: lakatos:proofs-and-refs.

[247]

Linda Lamb. Learning the vi Editor. O'Reilly & Associates, fifth edition, 1990.
Lib: SCS.
Key: lamb:vi.

[248]

Leslie Lamport. LaTeX User's Guide and Reference Manual. Addison-Wesley, second edition, 1994.
Lib: SCS.
Key: lamport:latex-guide.

[249]

Sidney I. Landau. Dictionaries: The Art and Craft of Lexicography. Cambridge University Press, 1989.
Lib: SCS.
Key: landau:dictionaries.

[250]

P. J. Landin. The next 700 programming languages. Communications of the ACM, 9(3):157-166, March 1966.
Lib: SCS-174.
Key: landin:700.

[251]

Susanne K. Langer. An Introduction to Symbolic Logic. Addison-Wesley, third revised edition, 1967.
Lib: SCS.
Key: langer:symbolic-logic.

[252]

John Launchbury. Self-applicable partial evaluation without S-expressions.
Lib: SCS-146.
Key: launchbury:self-appl-wo-s.

[253]

John Launchbury. A natural semantics for lazy evaluation. In Proceedings of POPL '93, 1993.
Lib: SCS-213.
Key: launchbury:lazy-sem.

[254]

Julia L. Lawall. Faster fourier transforms via automatic program specialization. In Hatcliff et al. [191], pages 81-93.
Lib: SCS.
Key: lawall:fft-program-spec.

[255]

Greg Lehey. Porting UNIX Software. O'Reilly & Associates, 1995.
Lib: SCS.
Key: lehey:porting-unix-sw.

[256]

Mary-Claire van Leunen. A Handbook for Scholars. Oxford University Press, revised edition, 1992.
Lib: SCS.
Key: vanleunen:handbook-scholars.

[257]

Michael Leuschel. Logic program specialization. In Hatcliff et al. [191], pages 159-205.
Lib: SCS.
Key: leuschel:logic-program-spec.

[258]

Michael Leuschel. On the power of homeomorphic embedding for online termination. In Proceedings of SAS '98, Lecture Notes in Computer Science. Springer-Verlag, 1998. To appear.
Lib: SCS-32.
Key: leuschel:homeomorphic-embedding.

[259]

John R. Levine, Tony Mason, and Doug Brown. lex & yacc. O'Reilly & Associates, second edition, 1992.
Lib: SCS.
Key: levine:lex-yacc.

[260]

Ming Li and Paul Vitányi. An Introduction to Kolmogorov Complexity and Its Applications. Graduate Texts in Computer Science. Springer-Verlag, second edition, 1997.
Lib: SCS.
Key: li:kolmogorov.

[261]

R. J. Lipton, S. C. Eisenstadt, and R. A. DeMillo. Space and time hierarchies for classes of control structures and data structures. Journal of the ACM, 23(4):720-732, October 1976.
Lib: SCS-195.
Key: lipton:compl-control-data.

[262]

Richard J. Lipton, Stanley C. Eisenstadt, and Richard A. DeMillo. Space-time trade-offs in structured programming: An improved combinatorial embedding theorem. Journal of the ACM, 27(1):123-127, January 1980.
Lib: SCS-196.
Key: lipton:tradeoff-control-data.

[263]

Ralph Loader. The undecidability of lambda -definability. To appear in the Church Memorial Volume.
Lib: SCS-221.
Key: loader:undec-lambda-def. (DVI)

[264]

Saunders Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer-Verlag, second edition, 1998.
Lib: SCS.
Key: maclane:categories.

[265]

Donald MacKenzie. The automation of proof: A historical and sociological exploration. Annals of the History of Computing, 17(3):7-29, 1995.
Lib: SCS-242.
Key: mackenzie:hist-ap.

[266]

John Maraist, Martin Odersky, and Philip Wadler. The call-by-need lambda calculus. Journal of Functional Programming, 8(3):275-317, May 1998.
Lib: SCS-211.
Key: mariast:call-by-need. (PostScript) (DVI)

[267]

Per Martin-Löf. Constructive mathematics and computer programming. In Logic, Methodology and Philosophy of Science, VI, 1979, pages 153-175. North-Holland, 1982.
Lib: SCS-224.
Key: martin-lof:constr-math-prog.

[268]

Per Martin-Löf. Intuitionistic Type Theory. Studies in Proof Theory. Bibliopolis, 1984.
Lib: SCS-223.
Key: martin-lof:intui-tt.

[269]

C. R. F. Maunder. Algebraic Topology. Van Nostrand Reinhold Company, 1970. Republished with corrections by Cambridge University Press in 1980, this, in turn, republished by Dover in 1996.
Lib: SCS.
Key: maunder:alg-top.

[270]

Steve McConnell. Code Complete: A Practical Handbook of Software Construction. Microsoft Press, 1993.
Lib: SCS.
Key: mcconnell:code-complete.

[271]

Elliott Mendelson. Introduction to Mathematical Logic. Chapman & Hall, fourth edition, 1997.
Lib: DIKU.
Key: mendelson:intro-logic.

[272]

Robin Milner. A theory of type polymorphism in programming.
Lib: SCS-156.
Key: milner:theory-typ-poly.

[273]

Robin Milner, Mads Tofte, and Robert Harper. The Definition of Standard ML. MIT Press, revised edition, 1997.
Lib: SCS.
Key: def:sml90.

[274]

John C. Mitchell. Type inference with simple subtypes. Journal of Functional Programming, 1(3):245-285, July 1991.
Lib: SCS-117.
Key: mitchell:type-inf-simple-subtypes.

[275]

John C. Mitchell. Foundations for Programming Languages. Foundations of Computing. MIT Press, 1996.
Lib: SCS.
Key: mitchell:found-prog-lang.

[276]

Torben Æ. Mogensen. Efficient self-interpretation in lambda calculus. Journal of Functional Programming, 2(3):345-364, July 1992.
Lib: SCS-99.
Key: mogensen:selfint. (PostScript) (DVI)

[277]

Torben Æ. Mogensen. Self-applicable partial evaluation for pure lambda calculus. In Charles Consel, editor, ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, pages 116-121. ACM, Yale University Press, 1992.
Lib: SCS-24.
Key: mogensen:offline-lambda. (PostScript) (DVI)

[278]

Torben Æ. Mogensen. Constructor specialization. In David Schmidt, editor, ACM Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pages 22-32. ACM Press, June 1993.
Lib: SCS-162.
Key: mogensen:constr-spec. (PostScript) (DVI)

[279]

Torben Æ. Mogensen. Self-applicable online partial evaluation of the pure lambda calculus. In William L. Scherlis, editor, Proceedings of PEPM '95, pages 39-44. ACM Press, 1995.
Lib: SCS-23.
Key: mogensen:online-lambda.

[280]

Torben Æ. Mogensen. Inherited limits. In Hatcliff et al. [191], pages 1-10.
Lib: SCS.
Key: mogensen:inherited-limits.

[281]

Torben Æ. Mogensen. Linear time self-interpretation of the pure lambda calculus, 1998. To appear.
Lib: SCS-96.
Key: mogensen:linear-lambda-selfint.

[282]

Torben Æ. Mogensen. Partial evaluation: Concepts and applications. In Hatcliff et al. [191], pages 1-20.
Lib: SCS.
Key: mogensen:partial-concepts-applications.

[283]

Eugenio Moggi. Notions of computation and monads. Information and Computation, 93(1):55-92, July 1991.
Lib: SCS-7.
Key: moggi:notions. (DVI)

[284]

Eugenio Moggi. A categorical account of two-level languages. In S. Brooks and M. Mislove, editors, MFPS XIII Mathematical Foundations of Programming Semantics, Thirteenth Annual Conference, volume 6 of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers, 1997.
Lib: SCS-11.
Key: moggi:cat-account-2lvl.

[285]

E. Moggi. Functor categories and two-level languages. In Maurice Nivat, editor, Foundations of Software Science and Computation Structures, volume 1378 of Lecture Notes in Computer Science, pages 211-225. Springer-Verlag, 1998.
Lib: SCS-2.
Key: moggi:func-cat-2lvl. (DVI)

[286]

Olaf Müller and Tobias Nipkow. Traces of I/O-automata in Isabelle/HOLCF. In M. Bidoit and M. Dauchet, editors, Theory and Practice of Software Development, volume 1214 of Lecture Notes in Computer Science, pages 580-594. Springer-Verlag, 1997.
Lib: SCS-76.
Key: muller:traces-io. (PostScript)

[287]

Olaf Müller and Konrad Slind. Isabelle/HOL as a platform for partiality, July 1996. Presented at the CADE-13 Workshop Mechanization of Partial Functions.
Lib: SCS-83.
Key: muller:isahol-partiality. (PostScript)

[288]

Olaf Müller and Konrad Slind. Treating partiality in a logic of total functions. The Computer Journal, 40(10), 1997.
Lib: SCS-155.
Key: muller:partiality. (PostScript)

[289]

Shigeru Muraki. Volumetric shape description of range data using ``blobby model''.
Lib: SCS-50.
Key: muraki:blobby.

[290]

Chetan R. Murthy. Classical logic as a programming language: Typing nonlocal control.
Lib: SCS-126.
Key: murthy:classical-logic-prog.

[291]

Alan Mycroft. Type-based decompilation (or program reconstruction via type reconstruction). In Swiestra [412], pages 208-223.
Lib: DIKU.
Key: mycroft:type-dec. (PostScript)

[292]

Wolfgang Naraschewski and Tobias Nipkow. Type inference verified: Algorithm W in Isabelle/HOL. Journal of Automated Reasoning, 1999. To appear.
Lib: SCS-71.
Key: naraschewski:w-inf. (DVI)

[293]

Peter Naur. Go to statements and good Algol style. BIT, 3:204-205, 1963.
Lib: SCS-194.
Key: naur:goto.

[294]

R. P. Nederpelt, J. H. Geuvers, and R. C. de Vrijer, editors. Selected Papers on Automath, volume 133 of Studies in Logic and the Foundations of Mathematics. North-Holland, 1994.
Lib: DNLB.
Key: nederpelt:automath.

[295]

Peter Møller Neergaard. Implementation of operational semantics. Student project, DIKU, March 1998.
Lib: SCS-15.
Key: neergaard:impl-os.

[296]

Peter Møller Neergaard. Towards inferring strong normalization from weak normalization for classical first order logic. Student project, DIKU, January 1999.
Lib: SCS-101.
Key: neergaard:strong-from-weak.

[297]

Peter Møller Neergaard and Morten Heine B. Sørensen. Conservation and uniform normalisation in lambda calculi with erasing reductions. Submitted for publication, 1999.
Lib: SCS-217.
Key: neergaard:cons-uni-norm.

[298]

Kristian Nielsen. A unified approach to partial evaluation and deforestation. Master's thesis, DIKU, Department of Computer Science, University of Copenhagen, September 1996.
Lib: SCS.
Key: nielsen:pe-deforestation.

[299]

Kristian Nielsen and Morten Heine Sørensen. Call-by-name CPS-translation as a binding-time improvement. In A. Mycroft, editor, Static Analysis Symposium, volume 983 of Lecture Notes in Computer Science, pages 296-313. Springer-Verlag, 1994.
Lib: SCS-38.
Key: nielsen:cps-deforestation. (PostScript)

[300]

Flemming Nielson. A formal type system for comparing partial evaluators. In Bjørner et al. [52], pages 349-384.
Lib: SCS-179.
Key: nielson:formal-type-comp-pe.

[301]

F. Nielson and H. R. Nielson. Two-Level Functional Languages, volume 34 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1992.
Lib: DIKU.
Key: nielson:two-lvl-func.

[302]

Tobias Nipkow. Isabelle/HOL: The Tutorial. Institut für Informatik, Technische Universität München, October 1998. Draft.
Lib: SCS-64.
Key: nipkow:isahol. (PostScript)

[303]

Tobias Nipkow. Verified lexical analysis. In Grundy and Newey [176].
Lib: SCS-77.
Key: nipkow:ver-la. (PostScript) (DVI)

[304]

Tobias Nipkow. Winskel is (almost) right: Towards a mechanized semantics textbook. Formal Aspects of Computing, 10:171-186, 1998.
Lib: SCS-70.
Key: nipkow:winskel. (PostScript) (DVI)

[305]

Henning Niss. An unfold/fold framework for first-order hereditary Harrop formulas: Transformations and correctness proofs. Master's thesis, DIKU, Department of Computer Science, University of Copenhagen, August 1997.
Lib: SCS-130.
Key: niss:horrap. (PostScript) (DVI)

[306]

Henning Niss and John Hatcliff. Formalizing operational semantics in logical frameworks: A case study using LF/Elf. In Bror Bjerner, Marie Larsson, and Bengt Nordström, editors, Proceedings of the 7th Nordic Workshop on Programming Theory, pages 277-297, Göteborg, Sweden, November 1995.
Lib: SCS-82.
Key: niss:form-op-sep. (PostScript) (DVI)

[307]

Bengt Nordström, Kent Petersson, and Jan M. Smith. Programming in Martin-Löf's Type Theory: An Introduction. Number 7 in The International Series of Monographs on Computer Science. Oxford University Press, 1990.
Lib: SCS.
Key: nordstrom:prog-ml-tt.

[308]

Donald A. Norman. The Design of Everyday Things. MIT Press, 1988.
Lib: SCS.
Key: norman:design-everyday-things.

[309]

Michael Norrish. Deterministic expressions in C. In Swiestra [412], pages 147-161.
Lib: SCS-180.
Key: norrish:det-exp-c.

[310]

Ole Fogh Olsen. Multi-scale segmentation of grey-scale images. Master's thesis, DIKU, Department of Computer Science, University of Copenhagen, 1996. DIKU Technical Report 96/30.
Lib: SCS.
Key: fogh-olsen:multi-scale. (PostScript)

[311]

Jaap van Oosten. Exercises in realizability. PhD thesis, University of Amsterdam, 1991.
Lib: SCS.
Key: oosten:ex-real.

[312]

Jaap van Oosten. Basic category theory. Technical Report LS-95-1, BRICS, Department of Computer Science, University of Aarhus, January 1995.
Lib: SCS-137.
Key: oosten:basic-cat-theory. (PostScript) (DVI)

[313]

Andrew Oram and Steve Talbott. Managing Projects with make. O'Reilly & Associates, second edition, 1991.
Lib: SCS.
Key: oram:make.

[314]

Martin J. Osborne and Ariel Rubinstein. A Course in Game Theory. MIT Press, 1994.
Lib: SCS.
Key: osborne:game-theory.

[315]

S. Owre and N. Shankar. Abstract datatypes in PVS. Technical Report CSL-93-9R, Computer Science Laboratory, SRI International, 1997.
Lib: SCS-139.
Key: owre:abs-data-pvs. (PostScript) (DVI)

[316]

Sam Owre and Natarajan Shankar. The formal semantics of PVS. Technical Report CSL-97-2, Computer Science Laboratory, SRI International, 1997.
Lib: SCS-141.
Key: owre:form-sem-pvs. (PostScript) (DVI)

[317]

S. Owre, N. Shankar, J. M. Rushby, and D. W. J. Stringer-Calvert. PVS Language Reference. SRI International, 1998.
Lib: SCS.
Key: pvs:lang-ref. (PostScript)

[318]

S. Owre, N. Shankar, J. M. Rushby, and D. W. J. Stringer-Calvert. PVS System Guide. SRI International, 1998.
Lib: SCS.
Key: pvs:system-guide. (PostScript)

[319]

James G. Oxley. Matroid Theory, volume 3 of Oxford Graduate Texts in Mathematics. Oxford University Press, 1992.
Lib: SCS.
Key: oxley:matroid.

[320]

Jens Palsberg. Correctness of binding-time analysis. Journal of Functional Programming, 3(3):347-363, July 1993.
Lib: SCS-12.
Key: palsberg:correctness-bta. (PostScript)

[321]

Jens Palsberg. Eta-redexes in partial evaluation. In Hatcliff et al. [191], pages 97-108.
Lib: SCS.
Key: palsberg:eta-redexes.

[322]

Ian Parberry. A guide for new referees in theoretical computer science. Information and Computation, 112(1):96-116, July 1994.
Lib: SCS-107.
Key: parberry:referee. (PostScript)

[323]

Oren Patashnik. Designing BibTeX styles, February 1988.
Lib: SCS-105.
Key: patashnik:bibtex-design.

[324]

Oren Patashnik. BibTeX ing, February 1988.
Lib: SCS-106.
Key: patashnik:bibtexing.

[325]

Lawrence C. Paulson. The foundation of a generic theorem prover. Journal of Automated Reasoning, 5(3):363-397, 1989.
Key: paulson:found-gen-tp. (DVI)

[326]

Lawrence C. Paulson. Isabelle: The next 700 theorem provers. In Piergiorgio Odifreddi, editor, Logic and Computer Science, pages 361-386. Academic Press, 1990.
Lib: SCS-80.
Key: paulson:700. (PDF) (DVI)

[327]

Lawrence C. Paulson. Designing a theorem prover. In S. Abramsky, Dov M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 415-475. Oxford University Press, 1992.
Lib: SCS-81.
Key: paulson:design-tp. (PDF) (DVI)

[328]

Lawrence C. Paulson. A fixedpoint approach to (co)inductive and (co)datatype definitions. In Alan Bundy, editor, Automated Deduction---CADE-12, volume 814 of Lecture Notes in Artificial Intelligence, pages 148-161. Springer-Verlag, 1994.
Lib: SCS-58.
Key: paulson:fix-coi-cod. (PDF) (DVI)

[329]

Lawrence C. Paulson. ML for the Working Programmer. Cambridge University Press, second edition, 1996.
Lib: SCS.
Key: paulson:ml.

[330]

Lawrence C. Paulson. A simple formalization and proof for the mutilated chess board. Technical Report 394, University of Cambridge, Computer Laboratory, May 1996.
Lib: SCS-73.
Key: paulson:form-mut-chess. (PostScript) (PDF) (DVI)

[331]

Lawrence C. Paulson. Introduction to Isabelle. University of Cambridge, Computer Laboratory, 1998.
Lib: SCS-60.
Key: isabelle:intro. (DVI)

[332]

Lawrence C. Paulson. The Isabelle Reference Manual. University of Cambridge, Computer Laboratory, 1998.
Lib: SCS.
Key: isabelle:ref. (DVI)

[333]

Lawrence C. Paulson. Isabelle's Object-Logics. University of Cambridge, Computer Laboratory, 1998.
Lib: SCS.
Key: isabelle:obj-logic. (DVI)

[334]

Lawrence C. Paulson and Krzysztof Grabczewski. Mechanizing set theory: Cardinal arithmetic and the axiom of choice. Journal of Automated Reasoning, 17(3):291-323, December 1996.
Lib: SCS-74.
Key: paulson:mech-set-theory. (PostScript) (PDF)

[335]

Hans Køhling Pedersen. Decorating implicit surfaces.
Lib: SCS-46.
Key: pedersen:dec-imp-surf.

[336]

Hans Køhling Pedersen. A framework for interactive texturing on curved surfaces.
Lib: SCS-49.
Key: pedersen:int-text-curved.

[337]

Hans Køhling Pedersen. A framework for interactive texturing on curved surfaces. Master's thesis, DIKU, Department of Computer Science, University of Copenhagen, May 1996.
Lib: SCS-136.
Key: pedersen:masters.

[338]

Simon L. Peyton Jones. The Implementation of Functional Programming Languages. International Series in Computer Science. Prentice-Hall International, 1987.
Lib: DIKU.
Key: peyton:impl-fun.

[339]

Simon L. Peyton Jones and Philip Wadler. Imperative functional programming. In 20th ACM Symposium on Principles of Programming Languages. ACM Press, January 1993.
Lib: SCS-153.
Key: peyton:imp-fun-prog. (PostScript) (DVI)

[340]

Frank Pfenning. Partial polymorphic type inference and higher-order unification. In ACM Conference on Lisp and Functional Programming, pages 153-163. ACM Press, July 1988.
Lib: SCS-157.
Key: pfenning:part-poly-ti.

[341]

Frank Pfenning. The practice of logical frameworks. In Hélène Kirchner, editor, Trees in Algebra and Programming--CAAP '96. Proceedings, volume 1059 of Lecture Notes in Computer Science, pages 119-134. Springer-Verlag, 1996.
Lib: SCS-78.
Key: pfenning:practice-lf. (PostScript)

[342]

Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In Proceedings of the SIGPLAN '88 Conference on Programming Language Design and Implementation, pages 199-208, 1988.
Lib: SCS-57.
Key: pfenning:ho-abs-syntax. (PostScript)

[343]

Benjamin C. Pierce. Basic Category Theory for Computer Scientists. Foundations of Computing. MIT Press, 1991.
Lib: SCS-133.
Key: pierce:basic-category.

[344]

Andrew M. Pitts. Some notes on inductive and co-inductive techniques in the semantics of functional programs. Draft Version, 1994.
Lib: SCS-135.
Key: pitts:co-ind.

[345]

G. D. Plotkin. Call-by-name, call-by-value and the lambda -calculus. Theoretical Computer Science, 1(2):125-159, December 1975.
Lib: SCS-103.
Key: plotkin:name-value-lambda.

[346]

G. D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5(3):223-255, December 1977.
Lib: SCS-52.
Key: plotkin:lcf-prog.

[347]

Gordon D. Plotkin. A structural approach to operational semantics. DAIMI Technical Report FN-19, DAIMI, Department of Computer Science, University of Aarhus, September 1981.
Lib: SCS.
Key: plotkin:structural-os.

[348]

Robert Pollack. On extensibility of proof checkers. In P. Dybjer, B. Nordström, and J. Smith, editors, Types for Proofs and Programs, volume 996 of LNCS, pages 140-161. Springer-Verlag, 1995.
Lib: SCS-192.
Key: pollack:ext-proof-check.

[349]

Robert Pollack. How to believe a machine-checked proof. In Giovanni Sambin and Jan Smith, editors, Twenty-Five Years of Constructive Type Theory, Oxford Logic Guides. Clarendon Press, August 1998. Also found as BRICS Report RS-97-18.
Lib: SCS-113.
Key: pollack:believe-mech-proof. (PostScript)

[350]

L. S. Pontryagin. Foundations of Combinatorial Topology. Graylock Press, 1952. Translated from Russian by F. Bagemihl, H. Komm, and W. Seidel.
Lib: SCS.
Key: pontryagin:found-comb-top.

[351]

Ben Potter, Jane Sinclair, and David Till. An Introduction to Formal Specification and Z. International Series in Computer Science. Prentice-Hall International, second edition, 1996.
Lib: SCS.
Key: potter:intro-form-spec-z.

[352]

Jacob Weismann Poulsen and Peter Andreasen. Information theory 1948-1998: Universal source coding, January 1999.
Lib: SCS-6.
Key: poulsen:inf-theory.

[353]

William H. Press, Saul A. Teukolsky, William T. Verrerling, and Brian B. Flannery. Numerical Recipes in C: The Art of Scientific Programming. Cambridge University Press, second edition, 1992.
Lib: SCS.
Key: press:num-rec-c.

[354]

Willard Van Orman Quine. From a Logical Point of View. Harvard University Press, second revised edition, 1980.
Lib: SCS.
Key: quine:logical-pov.

[355]

Femke van Raamsdonk, Paula Severi, Morten Heine B. Sørensen, and Hongwei Xi. Perpetual reductions in lambda -calculus. Information and Computation, 149(2):173-225, March 1999.
Lib: SCS.
Key: raamsdonk:perpetual-reductions.

[356]

Ole Rasmussen. The Church-Rosser theorem in Isabelle: A proof porting experiment. Technical Report 364, University of Cambridge, Computer Laboratory, March 1995.
Lib: SCS-72.
Key: rasmussen:cr-isabelle. (PostScript)

[357]

Jakob Rehof. Polymorphic dynamic typing: Aspects of proof theory and inference. Master's thesis, DIKU, Department of Computer Science, University of Copenhagen, 1995. DIKU Technical Report 95/9.
Lib: SCS.
Key: rehof:poly-typ.

[358]

Elaine Rich. Artificial Intelligence. McGraw-Hill Series in Artificial Intelligence. McGraw-Hill, 1983.
Lib: SCS.
Key: rich:ai.

[359]

D. M. Ritchie. The development of the C language. ACM SIGPLAN Notices, 28(3):201-208, March 1993. Also found in [3].
Lib: SCS-181.
Key: ritchie:c-hist. (PostScript)

[360]

Abraham Robinson. Non-standard Analysis. Princeton Landmarks in Mathematics. Princeton University Press, second edition, 1974. Reprinted in 1996.
Lib: SCS.
Key: robinson:non-std-analysis.

[361]

J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23-41, January 1965.
Lib: SCS-216.
Key: robinson:resolution.

[362]

S. Romaguera and M. Schellekens. Quasi-metric properties of complexity spaces. To appear.
Lib: SCS-5.
Key: romaguera:quasi-metric. (PostScript)

[363]

Kristoffer H. Rose. Xy -pic user's guide, December 1996.
Lib: SCS-197.
Key: rose:xyuser.

[364]

Mads Rosendahl. Complete partial orders.
Lib: SCS-158.
Key: rosendahl:comp-part-ord.

[365]

J. Barkley Rosser. Highlights of the history of the lambda calculus. Annals of the History of Computing, 6(4):337-349, October 1984.
Lib: SCS-237.
Key: rosser:highlights-lambda.

[366]

Walter Rudin. Functional Analysis. International Series in Pure and Applied Mathematics. McGraw-Hill, second edition, 1991.
Lib: SCS.
Key: rudin:func-anal.

[367]

Piotr Rudnicki and Andrzej Trybulec. On equivalents of well-foundedness: An experiment in Mizar. Accepted for the special issue of Journal of Automated Reason on Formal Proof.
Lib: SCS-75.
Key: rudnicki:equiv-wf. (PostScript) (DVI)

[368]

John Rushby, Sam Owre, and N. Shankar. Subtypes for specifications: Predicate subtyping in PVS. IEEE Transactions on Software Engineering, 24(9):709-720, September 1998.
Lib: SCS-140.
Key: rushby:subtypes-pred-pvs. (PostScript) (DVI)

[369]

J. M. Rushby and D. W. J. Stringer-Calvert. A less elementary tutorial for the PVS specification and verification system. Technical Report CSL-95-10, Computer Science Laboratory, SRI International, 1996.
Lib: SCS.
Key: rushby:less-elem-tutorial. (PostScript)

[370]

Jean E. Sammet. The use of English as a programming language. Communications of the ACM, 9(3):228-230, March 1966.
Lib: SCS-173.
Key: sammet:english-programming.

[371]

Andre Scedrov. A guide to polymorphic types. In Logic and Computer Science, pages 387-420. Academic Press, 1990.
Lib: SCS-118.
Key: scedrov:guide-poly.

[372]

Helmut Schwichtenberg. Type theory, 1992. Lecture notes.
Lib: SCS-89.
Key: schwichtenberg:type-theory. (DVI)

[373]

Helmut Schwichtenberg. Proof theory, 1994. Lecture notes.
Lib: SCS-90.
Key: schwichtenberg:proof-theory. (DVI)

[374]

Dana S. Scott. Relating theories of the lambda -calculus. In Seldin and Hindley [379], pages 403-450.
Lib: SCS-233.
Key: scott:relating-lambda-theories.

[375]

Dana S. Scott. Domains for denotational semantics. In Mogens Nielsen and Erik Meineche Schmidt, editors, Automata, Languages and Programming, volume 140 of Lecture Notes in Computer Science, pages 577-613. Springer-Verlag, 1982.
Lib: SCS-1.
Key: scott:domains.

[376]

W. R. Scott. Group Theory. Prentice-Hall, 1964. Republished with corrections by Dover in 1987.
Lib: SCS.
Key: scott:group-theory.

[377]

Jens Peter Secher. C-mix--specialization of C programs. In Hatcliff et al. [191], pages 119-156.
Lib: SCS.
Key: secher:c-mix.

[378]

Jens Peter Secher. Perfect supercompilation. Master's thesis, DIKU, Department of Computer Science, University of Copenhagen, February 1999.
Lib: SCS-29.
Key: secher:perfect-super. (PostScript)

[379]

Jonathan P. Seldin and John Roger Hindley, editors. To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, 1980.
Lib: DIKU.
Key: seldin:curry-essays.

[380]

Peter Sestoft. The structure of a self-applicable partial evaluator. In H. Ganzinger and N. D. Jones, editors, Programs as Data Objects, volume 217 of Lecture Notes in Computer Science, pages 236-256. Springer-Verlag, 1986. DIKU Technical Report 85/11.
Lib: SCS.
Key: sestoft:struct-pe.

[381]

Peter Sestoft. Replacing function parameters by global variables. Master's thesis, DIKU, Department of Computer Science, University of Copenhagen, October 1988.
Lib: SCS-159.
Key: sestoft:glob-var. (PostScript)

[382]

N. Shankar. Proof search in the intuitionistic sequent calculus. In Deepak Kapur, editor, Automated Deduction---CADE-11, volume 607 of Lecture Notes in Computer Science, pages 522-536. Springer-Verlag, 1992.
Lib: SCS-79.
Key: shankar:pvs-proof-search. (DVI)

[383]

N. Shankar, S. Owre, J. M. Rushby, and D. W. J. Stringer-Calvert. PVS Prover Guide. SRI International, 1998.
Lib: SCS.
Key: pvs:prover-guide. (PostScript)

[384]

W. Sierpinski. Elementary Theory of Numbers, volume 31 of North-Holland Mathematical Library. North-Holland, 1988.
Lib: DIKU.
Key: sierpinski:theory-of-numbers.

[385]

Richard A. Silverman. Introductory Complex Analysis. Prentice-Hall, 1967. Republished by Dover in 1972.
Lib: SCS.
Key: silverman:intro-comp-anal.

[386]

Satnam Singh and Nicholas McKay. Partial evaluation of hardware.
Lib: SCS-33.
Key: singh:pe-hardware.

[387]

Jens U. Skakkebæk and N. Shankar. A duration calculus proof checker: Using PVS as a semantic framework. Technical Report CSL-93-10, Computer Science Laboratory, SRI International, 1997.
Lib: SCS-142.
Key: skakkebaek:dc-pvs. (PostScript) (DVI)

[388]

Sebastian Skalberg. A formal semantics of refal. Student project, DIKU, June 1998.
Key: skalberg:refal-5. (PostScript) (DVI)

[389]

Sebastian C. Skalberg. Errata for map theory, 1999. A list of corrections for  [170].
Key: skalberg:mt-errata. (PostScript) (DVI)

[390]

Sebastian C. Skalberg. Mechanical proof of the optimality of a partial evaluator. Master's thesis, DIKU, Department of Computer Science, University of Copenhagen, February 1999.
Key: skalberg:opt-lambdamix. (PostScript) (DVI)

[391]

Sebastian C. Skalberg. An Interactive Proof System for Map Theory. PhD thesis, University of Copenhagen, October 2002.
Key: skalberg:isabelle-mt. (PostScript) (PDF) (DVI)

[392]

Raymond M. Smullyan. Analytic natural deduction. The Journal of Symbolic Logic, 30(2):123-139, June 1965.
Lib: SCS-240.
Key: smullyan-analytic-nat-ded.

[393]

Raymond M. Smullyan. First-Order Logic. Number 43 in Ergebnisse der Mathematik und ihrer Grenzgebeite. Springer-Verlag, 1968. Republished with corrections by Dover in 1995.
Lib: SCS.
Key: smullyan:fo-logic.

[394]

Harald Søndergaard. Semantics-Based Analysis and Transformation of Logic Programs. PhD thesis, University of Copenhagen, 1989. A revised report is found as DIKU Technical Report 89/22.
Lib: SCS.
Key: sondergaard:sem-based-anal.

[395]

Harald Søndergaard and Peter Sestoft. Non-determinacy and its semantics. DIKU Technical Report 86/12, DIKU, Department of Computer Science, University of Copenhagen, 1986.
Lib: SCS.
Key: sondergaard:sem-non-det.

[396]

Harald Søndergaard and Peter Sestoft. Referential transparancy and allied notions. DIKU Technical Report 88/7, DIKU, Department of Computer Science, University of Copenhagen, 1988.
Lib: SCS.
Key: sondergaard:ref-trans.

[397]

Morten Heine Sørensen. A grammar-based data-flow analysis to stop deforestation. In S. Tison, editor, Colloqium on Trees in Algebra and Programming, volume 787 of Lecture Notes in Computer Science, pages 335-351. Springer-Verlag, 1994.
Lib: SCS-161.
Key: sorensen:grammar-stop-df. (PostScript)

[398]

Morten Heine Sørensen. Turchin's supercompiler revisited--an operational theory of positive information propagation. Master's thesis, DIKU, Department of Computer Science, University of Copenhagen, 1994. DIKU Technical Report 94/9.
Lib: SCS.
Key: sorensen:turchin. (PostScript)

[399]

Morten Heine Sørensen. Normalization in lambda -Calculus and Type Theory. PhD thesis, University of Copenhagen, 1997. DIKU Technical Report 95/27.
Lib: SCS.
Key: sorensen:lambda-norm. (PostScript)

[400]

Morten Heine Sørensen. Strong normalization from weak normalization in typed lambda -calculi. Information and Computation, 133(1):35-71, February 1997.
Lib: SCS.
Key: sorensen:strong-from-weak. (PostScript)

[401]

Morten Heine B. Sørensen. Convergence of program tansformers in the metric space of trees. In Hatcliff et al. [191], pages 41-65.
Lib: SCS.
Key: sorensen:convergence-program-transform. (PostScript)

[402]

Morten Heine Sørensen, Robert Glück, and Neil D. Jones. A positive supercompiler. Journal of Functional Programming, 6(6):811-838, November 1996.
Key: sorensen:pos-supercomp. (PostScript)

[403]

Morten Heine B. Sørensen and Pawel Urzyczyn. Lectures on the Curry-Howard isomorphism. DIKU Technical Report 98/14, DIKU, Department of Computer Science, University of Copenhagen, 1998.
Lib: SCS.
Key: sorensen:curry-howard. (PostScript)

[404]

Michael Sperber, Robert Glück, and Peter Thiemann. Bootstrapping higher-order program transformers from interpreters. In K. M. George, Janice H. Carroll, Dave Oppenheim, and Jim Hightower, editors, ACM Symposium on Applied Computing, pages 408-413. ACM Press, 1996.
Lib: SCS-35.
Key: sperber:bootstrap. (PostScript)

[405]

W. Richard Stevens. UNIX Network Programming. Prentice-Hall, 1990.
Lib: SCS.
Key: stevens:unix-net-prog.

[406]

Ian Stewart and David Tall. Complex Analysis. Cambridge University Press, 1983.
Lib: SCS.
Key: stewart:compl-anal.

[407]

Allen Stoughton. Mechanizing logical relations.
Lib: SCS-160.
Key: stoughton:mech-log-rel.

[408]

David William John Stringer-Calvert. Mechanical Verification of Compiler Correctness. PhD thesis, University of York, March 1998.
Lib: SCS-65.
Key: stringer-c:phd. (PostScript)

[409]

Bjarne Stroustrup. The C++ Programming Language. Addison-Wesley, second edition, 1991.
Lib: SCS.
Key: stroustrup:cpp-prog-lang.

[410]

Bjarne Stroustrup. The Design and Evolution of C++. Addison-Wesley, 1994.
Lib: SCS.
Key: stroustrup:design-evo-c.

[411]

Patrick Suppes. Axiomatic Set Theory. Van Nostrand, 1960. Republished with corrections by Dover in 1972.
Lib: SCS.
Key: suppes:axiom-set-theory.

[412]

S. Doaitse Swiestra, editor. Programming Languages and Systems, volume 1576 of Lecture Notes in Computer Science. Springer-Verlag, 1999.
Lib: DIKU.
Key: lncs:1576.

[413]

W. W. Tait. The substitution method. The Journal of Symbolic Logic, 30(2):175-192, June 1965.
Lib: SCS-241.
Key: tait:subst-method.

[414]

Akihiko Takano. Generalized partial computation using disunification to solve constraints.
Lib: SCS-145.
Key: takano:gen-pc-dis.

[415]

Akihiko Takano and Erik Meijer. Shortcut deforestation in calculational form. In Conference on Functional Programming Languages and Computer Architecture. ACM Press, 1995.
Lib: SCS-41.
Key: takano:shortcut-calc. (PostScript)

[416]

Paul Taylor. Commutative diagrams in TeX (version 4), July 1994.
Lib: SCS-176.
Key: taylor:comm-diag-tex.

[417]

Peter Thiemann. Aspects of the PGG system: Specialization for standard Scheme. In Hatcliff et al. [191], pages 109-128.
Lib: SCS.
Key: thiemann:spec-std-scheme.

[418]

Peter Thiemann and Robert Glück. The generation of a higher-order online partial evaluator. In M. Takeichi and T. Ida, editors, Fuji International Workshop on Functional and Logic Programming, pages 239-253. World Scientific, 1995.
Lib: SCS-39.
Key: thiemann:gen-ho-pe.

[419]

Peter Thiemann and Michael Sperber. Polyvariant expansion and compiler generators. In Bjørner et al. [51], pages 285-296.
Lib: SCS-34.
Key: thiemann:poly-exp.

[420]

Mikkel Thorup. All structured programs have small tree-width and good register allocation. Information and Computation, 142(2):159-181, May 1998.
Lib: SCS-202.
Key: thorup:struct-prog. (PostScript)

[421]

H. A. Thurston. The Number-System. Interscience Publishers Inc., New York, 1956.
Lib: DNLB.
Key: thurston:number-system.

[422]

Mads Tofte and Jean-Pierre Talpin. A theory of stack allocation in polymorphically typed languages. DIKU Technical Report 93/15, DIKU, Department of Computer Science, University of Copenhagen, 1993.
Lib: SCS.
Key: tofte:th-stack-alloc.

[423]

V. F. Turchin. The Phenomenon of Science. Columbia University Press, 1977. Translated from Russian by Brand Frentz.
Lib: NDJ.
Key: turchin:phenomenon.

[424]

Valentin F. Turchin. The language REFAL---the theory of compilation and metasystem analysis. Courant Computer Science Report 20, Courant Institute of Mathematical Sciences, New York University, February 1980.
Lib: NDJ.
Key: turchin:refal-report.

[425]

Valentin F. Turchin. The concept of a supercompiler. ACM Transactions on Programming Languages and Systems, 8(3):292-325, July 1986.
Lib: SCS-30.
Key: turchin:supercompilation.

[426]

Valentin F. Turchin. REFAL-5: programming guide and reference manual. New England Publishing Co., 1989.
Lib: NA.
Key: def:refal-5.

[427]

A. M. Turing. On computable numbers, with an application to the entscheidungsproblem. Proceedings of the London Mathematical Society, 42(2):230-265, 1936-7. Reprinted with corrections as appendix One in [162].
Lib: SCS-92.
Key: turing:comp-num-ent.

[428]

A. M. Turing. Computability and lambda -definability. The Journal of Symbolic Logic, 2(4):153-163, December 1937.
Lib: SCS-94.
Key: turing:comp-ldef.

[429]

A. M. Turing. The p-function in lambda -K-conversion. The Journal of Symbolic Logic, 2(4):164, December 1937.
Lib: SCS-93.
Key: turing:p-func-conv.

[430]

Pawel Urzyczyn. Computability in abstract structures. Course notes, 1997.
Lib: SCS-91.
Key: urzycyn:flowcourse.

[431]

Thierry Vallée. Map Theory et Antifoundation. PhD thesis, Université Paris VII, 2001.
Key: vallee:phd.

[432]

Philip Wadler. Listlessness is better than laziness: Lazy evaluation and garbage collection at compile-time. In ACM Symposium on Lisp and Functional Programming, 1984.
Lib: SCS-147.
Key: wadler:listlessness.

[433]

Philip Wadler. Deforestation: Transforming programs to eliminate trees. Theoretical Computer Science, 73(2):231-248, June 1990.
Lib: SCS-31.
Key: wadler:deforestation. (PostScript) (DVI)

[434]

Philip Wadler. The essence of functional programming, 1992. Invited talk at the 19th Symposium on Principles of Programming Languages.
Lib: SCS-4.
Key: wadler:essence. (PostScript) (DVI)

[435]

Philip Wadler. Lazy versus strict. ACM Computing Surveys, 28(2):318-320, June 1996.
Lib: SCS-212.
Key: wadler:lazy-vs-strict. (PostScript) (DVI)

[436]

Philip Wadler. How to declare an imperative. ACM Computing Surveys, 29(3):240-263, September 1997.
Lib: SCS-3.
Key: wadler:decl-imp. (PostScript) (DVI)

[437]

C. T. C. Wall. A Geometric Introduction to Topology. Addison-Wesley, 1972. Republished by Dover in 1993.
Lib: SCS.
Key: wall:geo-intro-topology.

[438]

Mitchell Wand. Specifying the correctness of binding-time analysis. Journal of Functional Programming, 3(3):365-387, July 1993.
Lib: SCS-13.
Key: wand:spec-correctness-bta.

[439]

Morten Welinder. Partial Evaluation and Correctness. PhD thesis, University of Copenhagen, 1997. DIKU Technical Report 98/13.
Lib: SCS.
Key: welinder:pe-correctness. (PostScript)

[440]

Jim Welsh and John Elder. Introduction to Pascal. International Series in Computer Science. Prentice-Hall International, third edition, 1988.
Lib: SCS.
Key: welsh:intro-pascal.

[441]

Markus Wenzel. The Isabelle System Manual. Institut für Informatik, Technische Universität München, October 1998.
Lib: SCS-61.
Key: isabelle:system. (DVI)

[442]

Markus Wenzel. Using Axiomatic Type Classes in Isabelle: a Tutorial. Institut für Informatik, Technische Universität München, October 1998.
Lib: SCS-63.
Key: isabelle:axiom. (DVI)

[443]

Hermann Weyl. The Continuum: A Critical Examination of the Foundation of Analysis. Thomas Jefferson University Press, 1987. Contains a translation of emph Der circulus vitiosus in der heutigen Begründung der Analysis by Stephen Pollard and Thomas Bole. Republished with corrections by Dover in 1994.
Lib: SCS.
Key: weyl:continuum.

[444]

Alfred North Whitehead and Bertrand Russell. Principia Mathematica. Cambridge University Press, second edition, 1927.
Key: whitehead:principia.

[445]

Alfred North Whitehead and Bertrand Russell. Principia Mathematica to *56. Cambridge University Press, 1962. Abridged version of [444]. Reprinted in the Cambridge Mathematical Library series in 1997, also by Cambridge University Press.
Lib: SCS.
Key: whitehead:principia-to-56.

[446]

J. Eldon Whitesitt. Boolean Algebra and Its Applications. Addison-Wesley, 1961. Republished by Dover in 1995.
Lib: SCS.
Key: whitesitt:bool-alg-app.

[447]

H. P. Williams. Model Buliding in Mathematical Programming. John Wiley & Sons, third revised edition, 1993.
Lib: SCS.
Key: williams:model-build.

[448]

H. P. Williams. Model Solving in Mathematical Programming. John Wiley & Sons, 1993.
Lib: SCS.
Key: williams:model-solv.

[449]

Glynn Winskel. The Formal Semantics of Programming Languages: An Introduction. Foundations of Computing. MIT Press, 1993.
Lib: SCS.
Key: winskel.

[450]

Andrew P. Witkin and Paul S. Heckbert. Using particles to sample and control implicit surfaces.
Lib: SCS-51.
Key: witkin:part-samp-control.

[451]

Larry Wos, Ross Overbeek, Ewing Lusk, and Jim Boyle. Automated Reasoning: Introduction and Applications. Prentice-Hall, 1984.
Lib: SCS.
Key: wos:ar-intro-app.

---

[Main][Contact][CV][Isabelle][Map Theory][Bibliography][Links]

Bibliography

---