Below is a selection of papers which report work done as part
of the Church Project.
|
[1]
|
Sébastien Carlier and J. B. Wells.
The algebra of expansion.
Draft corresponding roughly to an ITRS 2008 workshop talk, March
2008.
|
|
[2]
|
Henning Makholm and J. B. Wells.
Type inference, principal typings, and let-polymorphism for
first-class mixin modules.
In Proc. 10th Int'l Conf. Functional Programming, pages
156-167. ACM Press, September 2005.
|
|
[3]
|
Kevin Donnelly and Assaf J. Kfoury.
Some considerations on formal semantics for weak references.
Technical Report Don+Kfo:BUCS-TR-2005-X, Department of Computer
Science, Boston University, July 2005.
|
|
[4]
|
Kevin Donnelly, Joseph J. Hallett, and Assaf J. Kfoury.
Formal semantics for weak references.
Technical Report Don+Hal+Kfo:BUCS-TR-2005-X, Department of Computer
Science, Boston University, July 2005.
|
|
[5]
|
Joseph J. Hallett and Assaf J. Kfoury.
A formal semantics for weak references.
Technical Report Hal+Kfo:BUCS-TR-2005-031, Department of Computer
Science, Boston University, May 2005.
|
|
[6]
|
Adam Bakewell and Assaf J. Kfoury.
Properties of a rewrite system for unification with expansion
variables.
Technical report, Church Project, Boston University, April 2005.
|
|
[7]
|
Adam Bakewell, Sébastien Carlier, A. J. Kfoury, and J. B. Wells.
Inferring intersection typings that are equivalent to
call-by-name and call-by-value evaluations.
Technical report, Church Project, Boston University, April 2005.
|
|
[8]
|
Dengping Zhu and Hongwei Xi.
Safe programming with pointers through stateful views.
In Proceedings of the 7th International Symposium on Practical
Aspects of Declarative Languages, page TBA, Long Beach, CA, January 2005.
Springer-Verlag LNCS.
|
|
[9]
|
Henning Makholm and J. B. Wells.
Instant polymorphic type systems for mobile process calculi:
Just add reduction rules and close.
In Programming Languages & Systems, 14th European Symp. Programming, volume 3444 of LNCS, pages 389-407. Springer-Verlag,
2005.
A more detailed predecessor is [12].
|
|
[10]
|
Adam Bakewell and Assaf J. Kfoury.
Unification with expansion variables.
Technical report, Department of Computer Science, Boston University,
December 2004.
|
|
[11]
|
Adam Bakewell, Sébastien Carlier, A. J. Kfoury, and J. B. Wells.
Exact intersection typing inference and call-by-name
evaluation.
Technical report, Department of Computer Science, Boston University,
December 2004.
Superseded by [7].
|
|
[12]
|
Henning Makholm and J. B. Wells.
Instant polymorphic type systems for mobile process calculi:
Just add reduction rules and close.
Technical Report HW-MACS-TR-0022, Heriot-Watt Univ., School of Math. & Comput. Sci., November 2004.
A shorter successor is [9].
|
|
[13]
|
Peter Møller Neergaard.
A functional language for logarithmic space.
In Prog. Lang. and Systems: 2nd Asian Symp. (APLAS 2004),
volume 3302 of LNCS, pages 311-326. Springer-Verlag, November 2004.
|
|
[14]
|
Peter Møller Neergaard.
Complexity Aspects of Programming Language Design-From
Logspace to Elementary Time via Proofnets and Intersection Types.
PhD thesis, Brandeis University, October 2004.
|
|
[15]
|
Peter Møller Neergaard and Harry G. Mairson.
Types, potency, and idempotency: Why nonlinearity and amnesia
make a type system work.
In Proc. 9th Int'l Conf. Functional Programming. ACM Press,
September 2004.
|
|
[16]
|
Chiyan Chen, Dengping Zhu, and Hongwei Xi.
Implementing cut elimination: A case study of simulating
dependent types in Haskell.
In Proceedings of the 6th International Symposium on Practical
Aspects of Declarative Languages, pages 239-254, Dallas, TX, June 2004.
Springer-Verlag LNCS vol. 3057.
|
|
[17]
|
Chiyan Chen, Rui Shi, and Hongwei Xi.
A typeful approach to object-oriented programming with multiple
inheritance.
In Proceedings of the 6th International Symposium on Practical
Aspects of Declarative Languages, pages 23-38, Dallas, TX, June 2004.
Springer-Verlag LNCS vol. 3057.
|
|
[18]
|
Peter Møller Neergaard.
BC-epsilon: A recursion-theoretic
characterization of logspace.
Technical report, Brandeis University, March 2004.
Preliminary version.
|
|
[19]
|
Torben Amtoft, Henning Makholm, and J. B. Wells.
PolyA: True type polymorphism for Mobile Ambients.
Technical Report HW-MACS-TR-0015, Heriot-Watt Univ., School of Math. & Comput. Sci., February 2004.
A shorter successor is [24].
|
|
[20]
|
Joseph J. Hallett and Assaf J. Kfoury.
Programming examples needing polymorphic recursion.
Technical Report BUCS-TR-2004-004, Department of Computer Science,
Boston University, January 2004.
|
|
[21]
|
Hongwei Xi.
Applied type system (extended abstract).
In post-workshop Proceedings of TYPES 2003, pages 394-408.
Springer-Verlag LNCS 3085, 2004.
|
|
[22]
|
Peter Andrews, Matthew Bishop, Chad Brown, Sunil Issar, Frank Pfenning, and
Hongwei Xi.
Etps: A system to help students to write formal proofs.
Journal of Automated Reasoning, 32:75-92, 2004.
|
|
[23]
|
Henning Makholm and J. B. Wells.
Type inference for PolyA.
Technical Report HW-MACS-TR-0013, Heriot-Watt Univ., School of Math. & Comput. Sci., January 2004.
|
|
[24]
|
Torben Amtoft, Henning Makholm, and J. B. Wells.
PolyA: True type polymorphism for Mobile Ambients.
In IFIP TC1 3rd Int'l Conf. Theoret. Comput. Sci. (TCS
'04), pages 591-604. Kluwer Academic Publishers, 2004.
A more detailed predecessor is [19].
|
|
[25]
|
Christian Haack and J. B. Wells.
Type error slicing in implicitly typed higher-order languages.
Sci. Comput. Programming, 50:189-224, 2004.
Supersedes [41].
|
|
[26]
|
Sébastien Carlier, Jeff Polakow, J. B. Wells, and A. J. Kfoury.
System E: Expansion variables for flexible typing with
linear and non-linear types and intersection types.
In Programming Languages & Systems, 13th European Symp. Programming, volume 2986 of LNCS, pages 294-309. Springer-Verlag,
2004.
|
|
[27]
|
Sébastien Carlier and J. B. Wells.
Type inference with expansion variables and intersection types
in System E and an exact correspondence with beta-reduction.
In Proc. 6th Int'l Conf. Principles & Practice Declarative
Programming, 2004.
Completely supersedes [?].
|
|
[28]
|
Assaf J. Kfoury and J. B. Wells.
Principality and type inference for intersection types using
expansion variables.
Theoret. Comput. Sci., 311(1-3):1-70, 2004.
Supersedes [80]. For omitted proofs, see the
longer report [33].
|
|
[29]
|
Dengping Zhu and Hongwei Xi.
A typeful and tagless representation for xml documents.
In Proceedings of the First Asian Symposium on Programming
Languages and Systems, pages 89-104, Beijing, China, November 2003.
|
|
[30]
|
Walid Taha, Stephan Ellner, and Hongwei Xi.
Generating imperative, heap-bounded programs in a functional
setting.
In Proceedings of the Third International Conference on Embedded
Software, pages 340-355, Philadelphia, PA, October 2003. Springer-Verlag
LNCS 2855.
|
|
[31]
|
Hongwei Xi.
Facilitating program verification with dependent types.
In Proceedings of the International Conference on Software
Engineering and Formal Methods, pages 72-81, Brisbane, Australia, September
2003.
|
|
[32]
|
Chiyan Chen and Hongwei Xi.
Meta-programming through typeful code representation.
In Proceedings of the Eighth ACM SIGPLAN International
Conference on Functional Programming, pages 275-286, Uppsala, Sweden,
August 2003.
|
|
[33]
|
Assaf J. Kfoury and J. B. Wells.
Principality and type inference for intersection types using
expansion variables.
Supersedes [80], August 2003.
|
|
[34]
|
Chiyan Chen and Hongwei Xi.
Implementing typeful program transformation.
In Proceedings of ACM SIGPLAN Workshop on Partial Evaluation and
Semantics Based Program Manipulation, San Diego, CA, June 2003.
|
|
[35]
|
Hongwei Xi.
Dependently typed pattern matching.
In Proceedings of Simposio Brasileiro de Linguagens de
Programacao, Ouro Preto, Brazil, May 2003.
|
|
[36]
|
J. B. Wells, Detlef Plump, and Fairouz Kamareddine.
Diagrams for meaning preservation.
Long version of [39], April 2003.
|
|
[37]
|
Hongwei Xi.
Dependently typed pattern matching.
Journal of Universal Computer Science, 9(8):851-872, 2003.
|
|
[38]
|
Hongwei Xi, Chiyan Chen, and Gang Chen.
Guarded recursive datatype constructors.
In Proceedings of the 30th ACM SIGPLAN Symposium on Principles
of Programming Languages, pages 224-235, New Orleans, January 2003.
|
|
[39]
|
J. B. Wells, Detlef Plump, and Fairouz Kamareddine.
Diagrams for meaning preservation.
In Rewriting Techniques & Applications, 14th Int'l Conf., RTA
2003, volume 2706 of LNCS, pages 88-106. Springer-Verlag, 2003.
A long version is [36].
|
|
[40]
|
Gang Chen.
Coercive subtyping for the calculus of constructions (extended
abstract).
In Conf. Rec. POPL '03: 30th ACM Symp. Princ. of Prog. Langs., 2003.
|
|
[41]
|
Christian Haack and J. B. Wells.
Type error slicing in implicitly typed higher-order languages.
In Programming Languages & Systems, 12th European Symp. Programming, volume 2618 of LNCS, pages 284-301. Springer-Verlag,
2003.
Superseded by [25].
|
|
[42]
|
Torben Amtoft and Robert Muller.
Inferring annotated types for inter-procedural register
allocation with constructor flattening.
In The 2003 ACM SIGPLAN International Workshop on Types in
Language Design and Implementation (TLDI'03), pages 86-97. ACM Press,
January 2003.
|
|
[43]
|
Peter Møller Neergaard and Harry G. Mairson.
How light is safe recursion? Translations between logics of
polynomial time.
Unpublished note, 2003.
|
|
[44]
|
Peter Møller Neergaard and Harry G. Mairson.
Rank bounded intersection: Types, potency, and idempotency.
This paper is obsolete and has been replaced with
[15], 2003.
|
|
[45]
|
Torben Amtoft and J. B. Wells.
Mobile processes with dependent communication types and
singleton types for names and capabilities.
Technical Report 2002-3, Kansas State University, Department of
Computing and Information Sciences, December 2002.
|
|
[46]
|
Hongwei Xi.
Dependent types for program termination verification.
Journal of Higher-Order and Symbolic Computation, 15:91-131,
October 2002.
|
|
[47]
|
Peter Møller Neergaard and Morten Heine B. Sørensen.
Conservation and uniform normalization in lambda-calculi with
erasing reductions.
Information and Computation, 178(1):149-179, October 2002.
|
|
[48]
|
Hongwei Xi.
Unifying Object-Oriented Programming with Typed Functional
Programming.
In Proceedings of ASIAN Symposium on Partial Evaluation and
Semantics-Based Program Manipulation (ASIA-PEPM), pages 117-125,
Aizu-Wakamatsu, Japan, September 2002.
|
|
[49]
|
Peter Møller Neergaard and Harry G. Mairson.
LAL is square: Representation and expressiveness in light
affine logic.
In Proc. Workshop on Implicit Computational Complexity, July
2002.
|
|
[50]
|
J. B. Wells, Allyn Dimock, Robert Muller, and Franklyn Turbak.
A calculus with polymorphic and polyvariant flow types.
J. Funct. Programming, 12(3):183-227, May 2002.
Supersedes [89].
|
|
[51]
|
Gang Chen.
Full integration of subtyping and if-expression.
In Proc. 4rd Int'l Conf. Principles & Practice Declarative
Programming. ACM Press, 2002.
|
|
[52]
|
Sébastien Carlier.
Polar type inference with intersection types and omega.
In Proceedings of the 2nd Workshop on Intersection Types and
Related Systems, 2002.
|
|
[53]
|
Assaf J. Kfoury, Geoff Washburn, and J. B. Wells.
Implementing compositional analysis using intersection types
with expansion variables.
In Proceedings of the 2nd Workshop on Intersection Types and
Related Systems, 2002.
|
|
[54]
|
Torben Amtoft, Assaf J. Kfoury, and Santiago M. Pericas-Geertsen.
Orderly communication in the ambient calculus.
Computer Languages, 28:29-60, 2002.
|
|
[55]
|
Torben Amtoft.
Causal type system for ambient movements.
Submitted for publication, 2002.
|
|
[56]
|
J. B. Wells.
The essence of principal typings.
In Proc. 29th Int'l Coll. Automata, Languages, and
Programming, volume 2380 of LNCS, pages 913-925. Springer-Verlag,
2002.
|
|
[57]
|
J. B. Wells.
The essence of principal typings.
A longer version of [56] with a 3-page appendix
with extra proofs, a page of extra discussion of non-related work, and other
minor changes, 2002.
|
|
[58]
|
J. B. Wells and Christian Haack.
Branching types.
In Programming Languages & Systems, 11th European Symp. Programming, volume 2305 of LNCS, pages 115-132. Springer-Verlag,
2002.
Completely superseded by [99].
|
|
[59]
|
Torben Amtoft, Charles Consel, Olivier Danvy, and Karoline Malmkjær.
The abstraction and instantiation of string-matching programs.
Technical Report BRICS RS-01-12, DAIMI, Department of Computer
Science, University of Aarhus, April 2001.
An extended version of an essay which appears in The Essence of
Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil
D. Jones, editors T. Mogensen and D. Schmidt and I. H Sudborough, Springer
LNCS 2566, pp 332-357, 2002.
|
|
[60]
|
Torben Amtoft, Assaf J. Kfoury, and Santiago M. Pericas-Geertsen.
What are polymorphically-typed ambients?
In David Sands, editor, ESOP 2001, Genova, volume 2028 of
LNCS, pages 206-220. Springer-Verlag, April 2001.
This downloadable extended summary is more detailed than the article
in the ESOP proceedings. A full report is [66].
|
|
[61]
|
Allyn Dimock, Ian Westmacott, Robert Muller, Franklyn Turbak, J. B. Wells, and
Jeffrey Considine.
Program representation size in an intermediate language with
intersection and union types.
Technical Report BUCS-TR-2001-02, Comp. Sci. Dept., Boston Univ.,
March 2001.
This is a version of [64]
extended with an appendix describing the CIL typed intermediate language.
|
|
[62]
|
Franklyn Turbak and J. B. Wells.
Cycle therapy: A prescription for fold and unfold on regular
trees.
In Proc. 3rd Int'l Conf. Principles & Practice Declarative
Programming, pages 137-149, 5-7 September 2001.
|
|
[63]
|
Santiago M. Pericas-Geertsen.
XML-Fluent Mobile Ambients.
PhD thesis, Boston University, 2001.
|
|
[64]
|
Allyn Dimock, Ian Westmacott, Robert Muller, Franklyn Turbak, J. B. Wells, and
Jeffrey Considine.
Program representation size in an intermediate language with
intersection and union types.
In Types in Compilation, Third Int'l Workshop, TIC 2000, volume
2071 of LNCS, pages 27-52. Springer-Verlag, 2001.
|
|
[65]
|
Allyn Dimock, Ian Westmacott, Robert Muller, Franklyn Turbak, and J. B. Wells.
Functioning without closure: Type-safe customized function
representations for Standard ML.
In Proc. 6th Int'l Conf. Functional Programming, pages
14-25. ACM Press, 2001.
|
|
[66]
|
Torben Amtoft, Assaf J. Kfoury, and Santiago M. Pericas-Geertsen.
What are polymorphically-typed ambients?
Technical Report BUCS-TR-2000-021, Comp. Sci. Dept., Boston Univ.,
December 2000.
|
|
[67]
|
Alan Bawden.
First-class macros have types.
In Conf. Rec. POPL '00: 27th ACM Symp. Princ. of Prog. Langs., pages 133-141, 2000.
|
|
[68]
|
Julia L. Lawall and Harry G. Mairson.
Sharing continuations: proofnets for languages with explicit
control.
In Programming Languages & Systems, 9th European Symp. Programming, volume 1782 of LNCS, pages 245-259. Springer-Verlag,
2000.
|
|
[69]
|
C. A. Stewart.
On the formulae-as-types correspondence for classical
logic.
PhD thesis, Oxford University, 2000.
|
|
[70]
|
Allyn Dimock, Ian Westmacott, Robert Muller, Franklyn Turbak, J. B. Wells, and
Jeffrey Considine.
Space issues in compiling with intersection and union types.
In Preliminary Proceedings of the Third Workshop on Types in
Compilation (TIC 2000), 2000.
Superseded by [64].
|
|
[71]
|
Assaf J. Kfoury.
A linearization of the lambda-calculus.
J. Logic Comput., 10(3):411-436, 2000.
Special issue on Type Theory and Term Rewriting. Kamareddine and Klop
(editors).
|
|
[72]
|
Michele Bugliesi and Santiago M. Pericas-Geertsen.
Type inference for variant object types.
Inform. & Comput., 2000.
|
|
[73]
|
Michele Bugliesi and Santiago M. Pericas-Geertsen.
Depth subtyping and type inference for object calculi.
In Proc. Seventh Workshop on Foundations of Object-Oriented
Languages, Boston, Mass., U.S.A., 2000.
|
|
[74]
|
Torben Amtoft and Franklyn Turbak.
Faithful translations between polyvariant flows and polymorphic
types.
In Programming Languages & Systems, 9th European Symp. Programming, volume 1782 of LNCS, pages 26-40. Springer-Verlag, 2000.
|
|
[75]
|
Torben Amtoft and Franklyn Turbak.
Faithful translations between polyvariant flows and polymorphic
types.
Technical Report BUCS-TR-2000-01, Comp. Sci. Dept., Boston Univ.,
2000.
Expanded full report of [74]. To appear
Fall 2000, but a DRAFT version is available.
|
|
[76]
|
Elena Machkasova and Franklyn A. Turbak.
A calculus for link-time compilation.
In Programming Languages & Systems, 9th European Symp. Programming, volume 1782 of LNCS, pages 260-274. Springer-Verlag,
2000.
|
|
[77]
|
Elena Machkasova and Franklyn Turbak.
A calculus for link-time compilation.
Technical report, Comp. Sci. Dept., Boston Univ., 2000.
Expanded full report of [76].
|
|
[78]
|
Torben Amtoft.
Partial evaluation for constraint-based program analyses.
Technical Report BRICS-RS-99-45, BRICS, Dept. of Computer Science,
University of Aarhus, 1999.
|
|
[79]
|
Assaf J. Kfoury, Harry G. Mairson, Franklyn A. Turbak, and J. B. Wells.
Relating typability and expressibility in finite-rank
intersection type systems.
In Proc. 1999 Int'l Conf. Functional Programming, pages
90-101. ACM Press, 1999.
|
|
[80]
|
Assaf J. Kfoury and J. B. Wells.
Principality and decidable type inference for finite-rank
intersection types.
In Conf. Rec. POPL '99: 26th ACM Symp. Princ. of Prog. Langs., pages 161-174, 1999.
Superseded by [28].
|
|
[81]
|
J. B. Wells.
Typability and type checking in System F are equivalent and
undecidable.
Ann. Pure Appl. Logic, 98(1-3):111-156, 1999.
|
|
[82]
|
Assaf J. Kfoury.
Beta-reduction as unification.
In D. Niwinski, editor, Logic, Algebra, and Computer Science (H.
Rasiowa Memorial Conference, December 1996), Banach Center Publication,
Volume 46, pages 137-158. Springer-Verlag, 1999.
Supersedes [92] but omits a few proofs included
in the latter.
|
|
[83]
|
Assaf J. Kfoury and Santiago M. Pericas-Geertsen.
Type inference for recursive definitions.
In Proc. 14th Ann. IEEE Symp. Logic in Comput. Sci., pages
119-128, July 1999.
|
|
[84]
|
Assaf J. Kfoury and Santiago M. Pericas-Geertsen.
Type inference for recursive definitions.
Technical report, Comp. Sci. Dept., Boston Univ., 1999.
Expanded full report of [83].
|
|
[85]
|
Peter Møller Neergaard.
Weak and strong normalization, K-redexes, and
first-order logic.
Master's thesis, DIKU, August, 1999.
DIKU Technical Report 99/11.
|
|
[86]
|
Franklyn Turbak, Allyn Dimock, Robert Muller, and J. B. Wells.
Compiling with polymorphic and polyvariant flow types.
In Proc. First Int'l Workshop on Types in Compilation, June
1997.
|
|
[87]
|
C.-H. L. Ong and C. A. Stewart.
A Curry-Howard foundation for functional computation with
control.
In Conf. Rec. POPL '97: 24th ACM Symp. Princ. of Prog. Langs., pages 215 - 217, 1997.
|
|
[88]
|
Anindya Banerjee.
A modular, polyvariant, and type-based closure analysis.
In Proc. 1997 Int'l Conf. Functional Programming, pages
1-10. ACM Press, 1997.
|
|
[89]
|
J. B. Wells, Allyn Dimock, Robert Muller, and Franklyn Turbak.
A typed intermediate language for flow-directed compilation.
In Proc. 7th Int'l Joint Conf. Theory & Practice of Software
Development, volume 1214 of LNCS, pages 757-771, 1997.
Superseded by [50].
|
|
[90]
|
Allyn Dimock, Robert Muller, Franklyn Turbak, and J. B. Wells.
Strongly typed flow-directed representation transformations.
In Proc. 1997 Int'l Conf. Functional Programming, pages
11-24. ACM Press, 1997.
|
|
[91]
|
Assaf J. Kfoury.
A linearization of the lambda-calculus.
A refereed version is [71]. This version was
presented at the Glasgow Int'l School on Type Theory & Term Rewriting,
September 1996.
|
|
[92]
|
Assaf J. Kfoury.
Beta-reduction as unification.
A refereed extensively edited version
is [82]. This preliminary version was presented at
the Helena Rasiowa Memorial Conference, July 1996.
|
|
[93]
|
J. B. Wells.
Typability is undecidable for F+eta.
Tech. Rep. 96-022, Comp. Sci. Dept., Boston Univ., March 1996.
|
|
[94]
|
J. B. Wells.
The undecidability of Mitchell's subtyping relation.
Tech. Rep. 95-019, Comp. Sci. Dept., Boston Univ., December 1995.
|
|
[95]
|
Trevor Jim.
Rank 2 type systems and recursive definitions.
Technical Report MIT/LCS/TM-531, Massachusetts Institute of
Technology, November 1995.
|
|
[96]
|
Trevor Jim.
What are principal typings and what are they good for?
Tech. memo. MIT/LCS/TM-532, MIT, 1995.
|
|
[97]
|
A. J. Kfoury and J. B. Wells.
New notions of reduction and non-semantic proofs of
beta-strong normalization in typed lambda-calculi.
In Proc. 10th Ann. IEEE Symp. Logic in Comput. Sci., pages
311-321, 1995.
|
|
[98]
|
Gang Chen.
Soundness of coercion in the calculus of constructions.
To appear in Journal of Logic and Computation.
|
|
[99]
|
J. B. Wells and Christian Haack.
Branching types.
Inform. & Comput., 200X.
Completely supersedes [58]. Accepted subject to
revisions.
|
|
[100]
|
Peter Møller Neergaard.
A bargain for intersection types: A simple strong normalization
proof.
J. Funct. Programming.
To appear.
|
