📄 http:^^www.cs.bu.edu^groups^church^bibliography^
字号:
Date: Tue, 14 Jan 1997 21:57:18 GMTServer: NCSA/1.5Content-type: text/html<HTML><HEAD><TITLE>The Church Project: A Functional Language Using Intersection Types</TITLE><link rev="made" href="http://cs-www.bu.edu/students/grads/jbw/Home.html"><link rev="made" href="http://www.bc.edu/bc_org/avp/csom/CS/Faculty/Muller/"></HEAD><body><H1>The <!WA0><a href="http://www.cs.bu.edu/groups/church/bibliography/default.html"> Church Project</a> Bibliography</H1>This bibliography is a compilation of books and papersthat are relevant to the project. Much of this bibliographyis derived from the WWW publication directoriesof existing ML projects. These directories include:<ul><li><!WA1><A href="http://foxnet.cs.cmu.edu/HomePage.html">The Fox Project</a>.<li><!WA2><A href="http://pauillac.inria.fr/cristal/">Project Crystal</a>.<li><!WA3><a href="http://www.cs.Princeton.EDU:80/faculty/appel/">Andrew Appel's Home Page</a>.<li><!WA4><a href="http://www.diku.dk/research-groups/topps/activities/mlkit.html">TheML Kit</a>.</ul>A selective snapshot of the aboveprojects was taken on August 21, 1995.The <!WA5><a href="http://www.cs.cmu.edu/afs/cs.cmu.edu/user/mleone/web/sml-list/sml-list.html"> SML Mailing list archive</a> has some interesting discussionson various aspects of SML.<h2> Type Theory </h2><p><ul><li>R. Harper and J. Mitchell.<!WA6><A HREF="http://www.cs.cmu.edu:8001/afs/cs/user/rwh/public/papers/xml.ps">On the type structure of Standard ML</A>.<cite>Trans. Programming Languages and Systems</cite>, 15(2):211--252,Apr. 1993.</ul><h3>Limits and Disadvantages of the ML Type Systemand Universal-Quantifier Polymorphism</h3><ul><li>A.J. Kfoury and J.B. Wells.A direct algorithm for type inference in the rank-2 fragment of the second-order lambda calculus.In <cite>Proc. 1994 ACM Conf. LISP and Functional Programming</cite>.An earlier version was <!WA7><a href="ftp://cs-ftp.bu.edu/techreports/93-017-finite-rank.ps.gz">B.U. C.S. Technical Report 93-017</a>.<li>A.J. Kfoury, J. Tiuryn, and P. Urzyczyn.An analysis of ML typability.<cite>J. ACM</cite>, 41(2), Mar. 1994.<li>A.J. Kfoury, J. Tiuryn, and P. Urzyczyn.Type reconstruction in the presence of polymorphic recursion.<cite>Trans. Programming Languages and Systems</cite>, 15(2), Apr. 1993.<li>J.B. Wells.Typability and type checking in the second-order lambda calculusare equivalent and undecidable.In <cite>Proc. 9th Ann. IEEE Symp. Logic in Computer Science</cite>, 1994.<li>A.J. Kfoury and J.B. Wells.<!WA8><a href="ftp://cs-ftp.bu.edu/techreports/94-006-polymorphic-abstraction.ps.gz">Adding Polymorphic Abstraction to ML</a>.Technical Report 94-006, Comp. Sci. Dept., Boston Univ., 1994.<li>L. Jategaonkar.<cite>ML with Extended Pattern Matching and Subtypes</cite>.Master's Thesis, MIT, 1989.<li>J.C. Mitchell, S. Meldal, and N. Madhav.<!WA9><a href="ftp://theory.stanford.edu/pub/jcm/modules-subtypes-popl91.dvi.Z">An extension of Standard ML modules with subtyping and inheritance</a>.In <cite>Proc. 18th ACM Symp. on Principles of Programming Languages</cite>,pp. 270--278, Jan. 1991.<li>Various people,<!WA10><a href="http://www.cs.bu.edu/groups/church/bibliography/93-sml-rectype.html"> Extract on recursive types </a> from the93 mailing list archive. (Reads from bottom to top.)</ul><h3>Benefits of Rank-2 Intersection Types</h3><ul><li>T. Jim.<!WA11><a href="ftp://theory.lcs.mit.edu/pub/trevor/principal-typings.ps.gz">What are principal typings and what are they good for?</a>.Technical Report MIT/LCS/TM-532, MIT, 1995.<li>T. Jim.<cite>Rank-2 Type Systems and Recursive Definitions</cite>.Technical Report MIT/LCS/TM-531, MIT, 1995.</ul><h3>General Background on Intersection Types</h3><ul><li>F. Cardone and M. Coppo.Two extensions of Curry's type inference system.In P. Odifreddi, ed., <cite>Logic and Computer Science</cite>.Academic Press, 1990.<li>S. van Bakel.Complete restrictions of the intersection type discipline.<cite>Theoretical Computer Science</cite>, 102(1), Aug. 1992.<li>S. van Bakel.<cite>Intersection Type Disciplines in Lambda Calculus andApplicative Term Rewriting Systems</cite>.Ph.D. Thesis, Mathematisch Centrum, Amsterdam, 1993.<li>T. Jim.A forthcoming technical report on higher-rank intersection types.</ul><h3>Background on Subtyping</h3><ul><li>J.C. Mitchell.Type inference with simple subtypes.<cite>J. Functional Programming</cite>, 1(3):245--286, 1991.<li>J. Mitchell.Polymorphic type inference and containment.<cite>Information and Computation</cite>, 76(2/3), Feb./Mar. 1988.<li>G. Longo, K. Milsted, and S. Soloviev.A logic of subtyping.<cite>Proc. 10th Ann. IEEE Symp. Logic in Computer Science</cite>, 1995.</ul><h3> Applications of Intersection Types </h3><ul><li>J.C. Reynolds.Preliminary design of the programming language Forsythe.Technical Report CMU-CS-88-159, Carnegie Mellon University, June 1988.<li>T. Freeman.<!WA12><a href="ftp://reports.adm.cs.cmu.edu/usr/anon/1994/CMU-CS-94-110.ps.Z">Refinement Types for ML</a>.Ph.D. Dissertation, Carnegie Mellon University, 1994.<li>A.B. Compagnoni and B.C. Pierce.<!WA13><A HREF="http://www.cl.cam.ac.uk/users/bcp1000/ftp/fomeet.ps.gz">Multiple Inheritance via Intersection Types</a>.To appear in <cite>MSCS</cite>. Earlier versions appeared asEdinburgh report ECS-LFCS-93-275 and K.U.N. report 93-18. <li>B.C. Pierce.<!WA14><A HREF="http://www.cl.cam.ac.uk/users/bcp1000/ftp/fmeet-journal.ps.gz">Intersection types and bounded polymorphism</a>.To appear in<cite>MSCS</cite>.An<!WA15><A HREF="http://www.cl.cam.ac.uk/users/bcp1000/ftp/fmeet-tlca.ps.gz">earlier version</a>appeared in <cite>Proc. Typed Lambda Calculus and Applications</cite>,Mar. 1993.</ul><h2> General Reading on ML </h2><ul><li>L.C. Paulson.<cite>ML for the Working Programmer</cite>.Cambridge University Press, 1991. (Reprinted in 1993.)<li>J.D. Ullman. <cite>Elements of ML Programming</cite>.Prentice-Hall, 1994.<li>R. Milner, M. Tofte, and R. Harper.<cite>The Definition of Standard ML</cite>.MIT Press.<li>R. Milner, M. Tofte, and R. Harper.<cite>Commentary on the Definition of Standard ML</cite>.MIT Press.<li>D. MacQueen.<cite><!WA16><a href="ftp://ftp.research.att.com/dist/ml/papers/92-lncs-macqueen.ps">Reflections on Standard ML</a></cite>.Springer-Verlag, 1992. LNCS.<li>The ML 2000 Group.<cite>The ML 2000 Manifesto</cite>.Unpublished Draft, 1992.<li>A.W. Appel.<!WA17><a href="ftp://ftp.cs.princeton.edu/reports/1992/364.ps.Z">A Critique of Standard ML</a>.Technical Report TR-364-92, Princeton University, Dec. 1991.Appeared in <cite>J. Functional Programming</cite>, 3(4):391-430, 1993.<li>R. Harper and P. Lee.<!WA18><A HREF="http://foxnet.cs.cmu.edu/papers/renewal.ps">Advanced Languages for Systems Software: The Fox Project in 1994</A>.Technical Report CMU-CS-FOX-94-01, 1994.</ul><h2> Language Features </h2>This (incomplete) section contains references to papers on features ofML that have been problematic in one way or another for the ML type system.<h3> Module Systems </h3><ul><li>X. Leroy.<!WA19><A HREF="file://ftp.inria.fr/INRIA/Projects/cristal/Xavier.Leroy/syntactic-generativity.dvi.gz">A syntactic theory of type generativity and sharing</a>.To appear in <cite>J. Functional Programming</cite>, 1995.<blockquote>This paper presents a purely syntactic account of type generativity andsharing -- two key mechanisms in the Standard ML module system -- andshows its equivalence with the traditional stamp-based description ofthese mechanisms. This syntactic description recasts the Standard MLmodule system in a more abstract, type-theoretic framework.</blockquote><li>S.K. Biswas.<!WA20><a href="http://www.cis.upenn.edu/~sbiswas/papers/hmodules.ps.Z">Higher-order functors with transparent signatures</a>.In <cite>Proceedings 22nd ACM SIGPLAN-SIGACT Symposium onPrinciples of Programming Languages</cite>, pp. 154--163, Jan. 1995.<li>D. MacQueen and M. Tofte.<!WA21><a href="ftp://ftp.research.att.com/dist/ml/papers/94-esop-macqueen.ps">A semantics for higher-order functors</a>.In <cite>Proc. European Symposium on Programming</cite>, 1994.<li>X. Leroy.<!WA22><A HREF="file://ftp.inria.fr/INRIA/Projects/cristal/Xavier.Leroy/applicative-functors.dvi.gz">Applicative functors and fully transparent higher-order modules</a>.In <cite>Proc. Principles of Programming Languages</cite>, 1995.<p><blockquote>We present a variant of the Standard ML module system where parameterizedabstract types (i.e. functors returning generative types) map provablyequal arguments to compatible abstract types, instead of generatingdistinct types at each application as in Standard ML. This extensionsolves the full transparency problem (how to give syntactic signatures forhigher-order functors that express exactly their propagation of typeequations), and also provides better support for non-closed codefragments.</blockquote><li>⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -