Karl Crary Robert Harper Derek Dreyer Carnegie Mellon University , 2002, submitted.
Karl Crary(CMU)
Kim Bruce (Williams
Colledge)
Dominic
Duggan (Stevens
Institute of Technology)
Matthias Felleisen
(Northeastern University)
Robert Harper(CMU)
Derek R. Dreyer (CMU)
Mark Jones
(Oregon Univsersity)
Mark
Lillibridge (former CMU, current Compaq)
Xavier Leroy
(Inria)
John Mitchell
(Standford University)
Dave MacQueen
(Bell Laboratory)
David
MacQueen (Ecole Polytechnique)
Benjamin
C. Pierce (University
of Pennsilvania)
Zhong Shao
(Yale University)
Jean-Pierre Talpin
(IRISA, INRIA)
Tom Hirschowitz
(INRIA Rocquencourt)
Mads Tofte
Claudio Russo (Edinburg
University)
Jonathan Aldrich
(University of Washinton)
Davide Ancona
(Dipartimento di Informatica e Scienze dell'Informazione)
Aleksey Nogin (Cornell
University)
Jason Hickey (Cornell
University)
Joe Wells (Church
Project)
Note:
Researcher name -> their homepage
University -> local paper collection
A Type System for Higher-Order Modules
Karl Crary Robert Harper Derek
Dreyer Carnegie Mellon University , 2002, submitted.
Toward
a Practical Type Theory for Recursive Modules.
Derek Dreyer, Robert Harper, and Karl Crary.
Carnegie Mellon University Computer Science
Department
Technical Report CMU-CS-01-112, March, 2001.
Karl Crary, Robert Harper, and Derek Dreyer. A
Type System for Higher-Order Modules. To appear, 2002
Symposium on Principles of Programming Languages
(POPL '02).
Transparent
and Opaque Interpretations of Data Types.
Karl Crary, Robert Harper, Perry Cheng, Leaf
Petersen, and Chris Stone.
Technical Report. November, 1998.
Robert Harper, John C. Mitchell, and
Eugenio Moggi.
Higher-order
modules and the phase distinction.
In Seventeenth ACM SIGACT-SIGPLAN Symposium on Principles
of Programming Languages, pages 341--354, San Francisco, January 1990.
http://citeseer.nj.nec.com/harper90higherorder.html
R. Harper and M. Lillibridge.
A
type theoretic approach to higher-order modules with sharing.
In Proc. 21st ACM Symp. on Principles of Programming Languages, pages
127--137. ACM Press, 1994. http://citeseer.nj.nec.com/harper94typetheoretic.html
Mark Lillibridge. Translucent
Sums: A Foundation for Higher-Order Module Systems. Ph.D. Thesis, School
of Computer Science, Carnegie Mellon University, Pittsburgh, PA, May 1997.
(Also
available as CMU-CS-97-122.)
Harper, R. and Mitchell, J. C. (1993)
On the type
structure of Standard ML. ACM Transactions on Programming Languages
and Systems, 15(2):211--252.
Jason Hickey. Modular Frameworks for Higher Order Logics.
Jason Hickey. A Predicative Type-Theoretic Interpretation of Objects,
Jason Hickey. Formal
Objects in Type Theory Using Very Dependent Types, in Foundations of
Object-Oriented Languages 3, 1996.
Constable, Robert L. and Jason Hickey, Nuprl's Class Theory and
Its Applications. Unpublished
manuscript, 2000. [PostScript]
Nuprl
Publications
Alexei Kopylov. Dependent
Intersection: A New Way of Defining Records in Type Theory.
Technical Report TR2000-1809, Computer Science Department, Cornell
University, August 2000
Submited to Theoretical Computer Science.
[20]J. B. Wells and René Vestergaard. Confluent equational
reasoning for linking with first-class primitive modules
(long version). A short version is [14]. Full
paper, 3 appendices of proofs, August 1999. (PostScript)
[14]J. B. Wells and René Vestergaard. Equational reasoning for
linking with first-class primitive modules. In
Programming Languages & Systems, 9th European
Symp. Programming, volume 1782 of LNCS, pages 412-428.
Springer-Verlag, 2000. A long version is [20].
(PostScript)
(PDF)
D. Duggan.
Type-Based
Hot Swapping of Running Modules (PDF).
Extended abstract in ACM
International Conference on Functional Programming (ICFP),
Florence, Italy, Sept 2001.
SIGPLAN Notices.
D. Duggan.
A mixin-based, semantics-based approach to implementing modular reusable
domain-specific
programming languages (PDF). In European Conference on Object-Oriented
Programming (ECOOP), Cannes, France, June 2000.
D. Duggan.
Modular type-based reverse engineering of parameterized
types in Java code.
ACM SIGPLAN Symposium on Object-Oriented Programming:
Systems, Languages and Applications (OOPSLA). Denver, Colorado, November
1999.
D. Duggan and C. Sourelis.
Mixin
modules.
ACM SIGPLAN International Conference on Functional Programming, Philadelphia,
Pennsylvania, May 1996.
D. Duggan and C. Sourelis. Module-based
mixin-based inheritance. Submitted for publication.
Viviana Bono, Amit Patel, and Vitaly Shmatikov
A
Core Calculus of Classes and Mixins
ECOOP'99, LNCS 1628, pp 43, 1999.
Sheng Liang, Paul Hudak, andMark P.
Jones
Monad
Transformers and Modular Interpreters,
In Conference Record of POPL'95: 22nd
ACM
SIGPLAN-SIGACT
Symposium on Principles of Programming Languages,
San Francisco,
CA, January 1995.
Mark P. Jones.
Functional
Programming with Overloading and Higher-Order Polymorphism
First International Spring School on Advanced
Functional
Programming Techniques, B{\aa}stad, Sweden,
Springer-Verlag Lecture
Notes in Computer Science 925, May 1995.
Mark P. Jones, A
system of constructor classes,
Proceedings of the conference on Functional programming languages and
computer
architecture, p.52-61, June 09-11, 1993, Copenhagen, Denmark
R.B. Findler and M. Flatt. Modular
object-oriented programming with units and mixins. In Intl. Conf. on
Functional Programming 1998, September 1998.
http://citeseer.nj.nec.com/findler98modular.html
D. MacQueen and M. Tofte.
A semantics for higher-order functors. Proc. 5th European Symp. on
Programming, Edinburgh. Springer LNCS 788, 409--423 (1994).
http://citeseer.nj.nec.com/33649.html
Zhong Shao.Transparent
Modules with Fully Syntactic Signatures. In Proc. 1999 ACM
SIGPLAN International Conference on Functional Programming (ICFP'99), Paris,
France, pages 220-232, September 1999. ©1999 ACM.
Zhong Shao. Parameterized
signatures and higher-order modules. Technical Report YALEU/DCS/TR-1161,
Dept. of Computer Science, Yale University, August 1998.
http://citeseer.nj.nec.com/shao98parameterized.html
Zhong Shao. Typed
Cross-Module Compilation. In Proc. 1998 ACM SIGPLAN International
Conference on Functional Programming (ICFP'98), Baltimore, Maryland, pages
141-152,
September 1998. ©1998 ACM.
Zhong Shao. Typed
Cross-Module Compilation (Extended Version). Technical Report
YALEU/DCS/TR-1126, Department of Computer Science, Yale University, June
1998.
Xavier Leroy. Applicative
functors and fully transparent higher-order modules. In 1995 ACM Symposium
on Principles of Programming Languages, pages 142--153, San Francisco,
CA, January 1995.
Xavier Leroy. A
modular module system, Journal of Functional Programming 10(3), 2000.
Full source code available in the Web
appendix.
Xavier Leroy. Objects
and classes versus modules in Objective Caml, invited talk given at
ICFP'99.
Nowak, D., Talpin, J.-P., Gautier, T.,
Le Guernic, P.
"An ML-like
module system for the synchronous language SIGNAL" European Conference
on Parallel Processing (EUROPAR'97). (c) Springer Verlag, August 1997.
J. Vouillon. Using modules as classes. In Informal Proceedings of the FOOL'5 Workshop, January 1998.
Tom Hirschowitz, Modules mixins : typage et compilation, september 2000, master's report for the DEA Programmation: Sémantique, Preuves et Langages.
Tom Hirschowitz, Modules mixins : typage et implantation, december 2000, talk at the journées FOC.
Tom Hirschowitz and Xavier Leroy, Mixin
modules in a call-by-value setting (long version), october 2001 (preliminary
version, available as PDF, compressed postscript
or compressed dvi).
Sylvain Boulmé, Thérèse Hardin et Renaud Rioboo,
Laboratoire d'Informatique de Paris 6
Modules,
Objets et Calcul Formel, JFLA99.
J. A. Bergstra Module
algebra
in Journal of the ACM (JACM) Volume 37 , Issue 2
(April 1990)
1 E. K. Blum , H. Ehrig , F. Parisi-Presicce,
Algebraic specification of modules and their basic interconnections,
Journal of Computer and System Sciences, v.34 n.2-3, p.293-339, April/June
1987
J. A. Bergstra , Jan Heering , Paul Klint,
Algebraic specification,
ACM Press, New York, NY, 1989
Modules
in LOOM: Classes are not enough
by Kim B. Bruce, Leaf Petersen, and Joseph
Vanderwaart
Extended abstract. Last revised 4/13/98.
Mark Shields and Simon Peyton Jones. First-class
Modules for Haskell. Submitted to the Ninth International Conference
on Foundations of Object-Oriented Languages (FOOL 9), Portland, Oregon.
20 pages. Oct 2001. [A4 ps] [A4 pdf] [bibtex]
Davide Ancona and Elena Zucca
True
Modules for Java-like Languages
ECOOP 2001, LNCS 2072, pp 354, 2001.
Others
J.
H. Reppy and J.
G. Riecke. Classes
in Object ML via modules. In Third Workshop on Foundations of
ObjectOriented Languages, July 1996.
Masahiko Sato, "Theory
of Judgments and Derivations", to appear in Arikawa, S. and Shinohara,
A. eds., Progress in Discovery Science, Lecture Notes in
Artificial Intelligence, State-of-the-Art
Surveys, Springer, 2001. ps file.
Sound
and Complete Elimination of Singleton Kinds.
Karl Crary.
2000 Workshop on Types in Compilation.
Foundations
for the Implementation of Higher-Order Subtyping.
Karl Crary.
1997, International Conference on Functional
Programming.
Typed
Compilation of Inclusive Subtyping.
Karl Crary.
2000 International Conference on Functional
Programming.
Foundations
for the Implementation of Higher-Order Subtyping.
Karl Crary.
1997, International Conference on Functional
Programming.
Yong Luo , Zhaohui Luo
Coherence
and Transitivity in Coercive Subtyping
Volume 2250,
Issue , pp 0249-
Lecture Notes
in Artificial Intellingence
Alexandre Miquel
The
Implicit Calculus of Constructions
Volume 2044,
Issue , pp 0344-
Gilles Barthe , Femke van
Constructor
Subtyping in the Calculus of Inductive Constructions
Volume 1784,
Issue , pp 0017-
Lecture Notes
in Computer Science
David Aspinall
Subtyping with Power Types
Volume 1862,
Issue , pp 0156-
Lecture Notes
in Computer Science
Programming
Language Semantics in Foundational Type Theory.
Karl Crary.
1998 International Conference on Programming
Concepts and Methods.
Mark Jones.
Typing
Haskell in Haskell
In Proceedings of the 1999 Haskell
Workshop, Paris, France, October 1999. Published
in Technical Report
UU-CS-1999-28, Department of Computer Science,
University of Utrecht.
Type
Classes with Functional Dependencies,
Mark P. Jones,
In Proceedings of the 9th European Symposium
on Programming, ESOP 2000, Berlin, Germany,
March 2000, Springer-Verlag LNCS 1782.
Flemming
Nielson , HanneRiis Nielson
Type
and Effect Systems
Volume
1710, Issue , pp 0114-, Lecture Notes in Computer Science
Konstantin Laufer, Combining
Type Classes and Existential Types, Proc. Latin American Informatics
Conference (PANEL),
ITESM-CEM, Mexico, September 1994. http://citeseer.nj.nec.com/laufer94combining.html
PhD
thesis: Dependent Record Types and Algebraic Structures in Type Theory
Department of Computing Science, Chalmers
University of Technology and University of Göteborg, Göteborg,
Sweden, February 1998.
Dependent
Record Types, Subtyping and Proof Reutilization
Presented at the workshop on "Subtyping, inheritance
and modular development of proofs", held at Durham,
England, 1997.
Extension
of Martin-Löf's type theory with record types and subtyping. (with
Alvaro Tasistro)
To appear in "25 Years of Constructive Type
Theory", Oxford University Press, 1997.
Robert Pollack. Dependently
typed records for representing mathematical structure. In Aagard and
Harrison, editors, Theorem Proving in
Higher Order Logics, TPHOLs 2000, volume 1869 of Lecture Notes in Computer
Science. SpringerVerlag, August 2000.
http://citeseer.nj.nec.com/pollack00dependently.html
J. Courant. An
applicative module calculus. In M. Bidoit and M. Dauchet, editors,
Proc. TAPSOFT '97: Theory and Practice of Software
Development, Lecture Notes in Computer Science, pages 622--636. Springer
Verlag, April 1997.
http://citeseer.nj.nec.com/courant97applicative.html
J. Courant. A
module calculus enjoying the subject-reduction property. To appear
in Proc. TAPSOFT '97: Theory and Practice of
Software Development, 1997. http://citeseer.nj.nec.com/courant96module.html
Judicael Courant. A
module calculus for pure type systems. In Typed Lambda Calculi and
Applications 97, LNCS. Springer-Verlag,
1997. http://citeseer.nj.nec.com/article/courant96module.html
More
Karl Crary. Type-Theoretic
Methodology for Practical Programming Languages. August 1998.
Xavier Leroy. Polymorphic
typing of an algorithmic language. Research report 1778, INRIA, 1992.
M. Lillibridge. Translucent
Sums: A Foundation for Higher-Order Module Systems. PhD thesis, School
of Computer Science, Carnegie Mellon University, 1997. Available as
technical report CMS-CS-97-122. http://citeseer.nj.nec.com/lillibridge97translucent.html
Honors theses
guided by Professor Kim Bruce
Adaptation in HOT Languages: Comparing Polymorphism, Modules, and Objects by David MacQueen.
Type
Systems: a tutorial on type systems by Luca Cardelli.
Essentials of Standard ML Modules: a tutorial on the Standard ML module
system. The postscript file at that page is suspect so here is
another copy derived from the dvi version.
The
Development of Type Systems for Object-Oriented Languages: a tutorial
on models for the type systems for
object-oriented languages.
Theories des types. (by Dowek )
Concepts
of Programming Languages (CS 320) (by Assaf Kfoury)
H.P. Barendregt . The Lambda Calculus: Its Syntax and Semantics , Elsevier Science, 1984.
Constable, et alii: Implementing Mathematics with The Nuprl Proof Development System
DejaVU Principles of Object-Oriented Software Development
Program Analyses: A Consumer's Perspective
abstractPPT
Invited Talk: Static Analysis Symposium
Contracts for Software Components (Work in Progress)
abstractPPT
Building Extensible Software
abstractPPT
Computer
Science Departments and Research Divisions (by J. Mitchell)
Professional
Organizations, Archives, Conference, Journal and Publisher Pages
Home Page for Intersection
Types and Related System
Church Project