| [1] | Martín Abadi and Luca Cardelli. A theory of primitive objects: Second-order systems. Science of Computer Programming, 25(2-3):81-116, December 1995. [ bib | .pdf ] |
| [2] | Martín Abadi and Luca Cardelli. A theory of primitive objects: Untyped and first-order systems. Information and Computation, 125(2):78-102, March 1996. [ bib | .pdf ] |
| [3] | Martín Abadi and Marcelo P. Fiore. Syntactic considerations on recursive types. In IEEE Symposium on Logic in Computer Science (LICS), pages 242-252, July 1996. [ bib | .ps ] |
| [4] | Martín Abadi, Anindya Banerjee, Nevin Heintze, and Jon G. Riecke. A core calculus of dependency. In ACM Symposium on Principles of Programming Languages (POPL), pages 147-160, January 1999. [ bib | .ps ] |
| [5] | Martín Abadi and Bruno Blanchet. Secrecy types for asymmetric communication. In International Conference on Foundations of Software Science and Computation Structures (FOSSACS), volume 2030 of Lecture Notes in Computer Science, pages 25-41. Springer Verlag, April 2001. [ bib | .html ] |
| [6] | Martín Abadi, Butler Lampson, and Jean-Jacques Lévy. Analysis and caching of dependencies. In ACM International Conference on Functional Programming (ICFP), pages 83-91, May 1996. [ bib | .ps ] |
| [7] | Martín Abadi, Benjamin Pierce, and Gordon Plotkin. Faithful ideal models for recursive polymorphic types. International Journal of Foundations of Computer Science, 2(1):1-21, March 1991. [ bib | .ps ] |
| [8] | Andreas Abel, Marcin Benke, Ana Bove, John Hughes, and Ulf Norell. Verifying Haskell programs using constructive type theory. In Haskell workshop, pages 62-73, September 2005. [ bib | .pdf ] |
| [9] | Samson Abramsky. Domain theory in logical form. Annals of Pure and Applied Logic, 51:1-77, 1991. [ bib | .ps.gz ] |
| [10] | Peter Achten and Marinus J. Plasmeijer. The ins and outs of Clean I/O. Journal of Functional Programming, 5(1):81-110, 1995. [ bib | .ps.gz ] |
| [11] | Sten Agerholm. A HOL basis for reasoning about functional programs. Technical Report RS-94-44, BRICS, December 1994. [ bib | .ps.gz ] |
| [12] | Sten Agerholm. LCF examples in HOL. Technical Report RS-94-18, BRICS, June 1994. [ bib | .ps.gz ] |
| [13] | Alfred Aho, Ravi Sethi, and Jeffrey Ullman. Compilateurs: principes, techniques et outils. InterEditions, 1989. [ bib ] |
| [14] | Alfred V. Aho, Ravi Sethi, and Jeffrey D. Ullman. Compilers: Principles, techniques, and tools. Addison-Wesley, 1986. [ bib ] |
| [15] | Alexander Aiken. Introduction to set constraint-based program analysis. Science of Computer Programming, 35:79-111, 1999. [ bib | .ps ] |
| [16] | Alexander Aiken, Manuel Fähndrich, and Raph Levien. Better static memory management: improving region-based analysis of higher-order languages. ACM SIGPLAN Notices, 30(6):174-185, June 1995. [ bib | .ps ] |
| [17] | Alexander Aiken, Manuel Fähndrich, Jeffrey S. Foster, and Zhendong Su. A toolkit for constructing type- and constraint-based program analyses. Lecture Notes in Computer Science, 1473:76-96, 1998. [ bib | .ps ] |
| [18] | Alexander S. Aiken. The Illyria system, 1994. [ bib | .html ] |
| [19] | Alexander S. Aiken and Manuel Fähndrich. Making set-constraint based program analyses scale. Technical Report CSD-96-917, University of California, Berkeley, September 1996. [ bib | .ps.gz ] |
| [20] | Alexander S. Aiken and Manuel Fähndrich. Subtyping polymorphic constrained types. Technical Report CSD-96-898, University of California, Berkeley, March 1996. [ bib ] |
| [21] | Alexander S. Aiken and Manuel Fähndrich. Program analysis using mixed term and set constraints. In Static Analysis Symposium (SAS), pages 114-126, September 1997. [ bib | .ps ] |
| [22] | Alexander S. Aiken and Edward L. Wimmers. Solving systems of set constraints. In IEEE Symposium on Logic in Computer Science (LICS), pages 329-340, June 1992. [ bib | .ps ] |
| [23] | Alexander S. Aiken and Edward L. Wimmers. Type inclusion constraints and type inference. In Conference on Functional Programming Languages and Computer Architecture (FPCA), pages 31-41. ACM Press, 1993. [ bib | .ps ] |
| [24] | Alexander S. Aiken, Edward L. Wimmers, and T. K. Lakshman. Soft typing with conditional types. In ACM Symposium on Principles of Programming Languages (POPL), pages 163-173, January 1994. [ bib | .ps ] |
| [25] | Alexander S. Aiken, Edward L. Wimmers, and Jens Palsberg. Optimal representations of polymorphic types with subtyping. Technical Report CSD-96-909, University of California, Berkeley, July 1996. [ bib | .ps ] |
| [26] | Thorsten Altenkirch, Conor McBride, and James McKinna. Why dependent types matter. Unpublished, April 2005. [ bib | .pdf ] |
| [27] | Roberto M. Amadio and Luca Cardelli. Subtyping recursive types. ACM Transactions on Programming Languages and Systems, 15(4):575-631, September 1993. [ bib | .pdf ] |
| [28] | Gregory R. Andrews. Foundations of multithreaded, parallel, and distributed programming. Addison-Wesley, 2000. [ bib ] |
| [29] | Gregory R. Andrews and Richard P. Reitman. An axiomatic approach to information flow in programs. ACM Transactions on Programming Languages and Systems, 2(1):56-76, January 1980. [ bib ] |
| [30] | Peter B. Andrews. An introduction to mathematical logic and type theory: to truth through proof. Academic Press, 1986. [ bib ] |
| [31] | Maria-Virginia Aponte and Roberto Di Cosmo. Type isomorphisms for module signatures. In Programming Languages: Implementations, Logics, and Programs (PLILP), volume 1140 of Lecture Notes in Computer Science, pages 334-346. Springer Verlag, September 1996. [ bib | http ] |
| [32] | Andrew Appel. Modern compiler implementation in ML. Cambridge University Press, 1998. [ bib | http ] |
| [33] | Krzysztof R. Apt. Ten years of Hoare's logic: A survey-part I. ACM Transactions on Programming Languages and Systems, 3(4):431-483, 1981. [ bib | http ] |
| [34] | André Arnold and Maurice Nivat. The metric space of infinite trees. Algebraic and topological properties. Fundamenta Informaticæ, 3(4):181-205, 1980. [ bib ] |
| [35] | Lennart Augustsson. Implementing Haskell overloading. In Conference on Functional Programming Languages and Computer Architecture (FPCA), pages 65-73, 1993. [ bib | .ps.Z ] |
| [36] | Jean-Michel Autebert. Théorie des langages et des automates. Masson, 1994. [ bib ] |
| [37] | Jean-Michel Autebert, Jean Berstel, and Luc Boasson. Context-free languages and push-down automata. In Handbook of Formal Languages, volume 1, pages 111-174. Springer Verlag, 1997. [ bib | .ps.gz ] |
| [38] | Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. Mechanized metatheory for the masses: The PoplMark challenge. In International Conference on Theorem Proving in Higher Order Logics (TPHOLs), Lecture Notes in Computer Science. Springer Verlag, August 2005. [ bib | .pdf ] |
| [39] | Henry G. Baker. Unify and conquer (garbage, updating, aliasing, ...) in functional languages. In ACM Symposium on Lisp and Functional Programming (LFP), pages 218-226, June 1990. [ bib | .ps.gz ] |
| [40] | Vincent Balat, Roberto Di Cosmo, and Marcelo Fiore. Remarks on isomorphisms in typed lambda calculi with empty and sum type. In IEEE Symposium on Logic in Computer Science (LICS), July 2002. [ bib | .ps.gz ] |
| [41] | Anindya Banerjee, Nevin Heintze, and Jon G. Riecke. Region analysis and the polymorphic lambda calculus. In IEEE Symposium on Logic in Computer Science (LICS), pages 88-97, July 1999. [ bib | .pdf ] |
| [42] | Anindya Banerjee, Nevin Heintze, and Jon G. Riecke. Design and correctness of program transformations based on control-flow analysis. In International Symposium on Theoretical Aspects of Computer Software (TACS), volume 2215 of Lecture Notes in Computer Science, pages 420-447. Springer Verlag, October 2001. [ bib | .ps.gz ] |
| [43] | Anindya Banerjee and David Naumann. Secure information flow and pointer confinement in a Java-like language. In IEEE Computer Security Foundations Workshop, pages 253-267, June 2002. [ bib | .ps ] |
| [44] | Anindya Banerjee and David A. Naumann. A simple semantics and static analysis for Java security. Technical Report 2001-1, Stevens Institute of Technology, June 2001. [ bib | .ps ] |
| [45] | Anindya Banerjee and David A. Naumann. Representation independence, confinement, and access control. In ACM Symposium on Principles of Programming Languages (POPL), pages 166-177, January 2002. [ bib | .ps ] |
| [46] | Jean-Pierre Banâtre, Ciarán Bryce, and Daniel Le Métayer. Compile-time detection of information flow in sequential programs. In European Symposium on Research in Computer Security, volume 875 of Lecture Notes in Computer Science, pages 55-74. Springer Verlag, 1994. [ bib | .ps.Z ] |
| [47] | Henk P. Barendregt. Functional programming and lambda calculus. In J. Van Leeuwen, editor, Handbook of Theoretical Computer Science, pages 321-363. Elsevier Science, 1990. [ bib ] |
| [48] | Erik Barendsen and Sjaak Smetsers. Uniqueness type inference. In Programming Languages: Implementations, Logics, and Programs (PLILP), volume 982 of Lecture Notes in Computer Science, pages 189-206. Springer Verlag, 1995. [ bib | http ] |
| [49] | Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte. The Spec# programming system: An overview. In International Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart devices (CASSIS), volume 3362 of Lecture Notes in Computer Science. Springer Verlag, 2004. [ bib | .pdf ] |
| [50] | Mike Barnett, David A. Naumann, Wolfram Schulte, and Qi Sun. 99.44% pure: Useful abstractions in specifications. In Formal Techniques for Java-like Programs, 2004. [ bib | .pdf ] |
| [51] | Chris Barrett, Riko Jacob, and Madhav Marathe. Formal language constrained path problems. SIAM Journal on Computing, 30(3):809-837, 2000. [ bib | .ps.gz ] |
| [52] | Frank Bartels, Friedrich von Henke, Holger Pfeifer, and Harald Rueß. Mechanizing domain theory. Ulmer Informatik-Berichte 96-10, Universität Ulm, Fakultät für Informatik, 1996. [ bib | .ps.gz ] |
| [53] | Massimo Bartoletti, Pierpaolo Degano, and GianLuigi Ferrari. Static analysis for stack inspection. In International Workshop on Concurrency and Coordination, volume 54 of Electronic Notes in Theoretical Computer Science. Elsevier Science, 2001. [ bib ] |
| [54] | Mike Beaven and Ryan Stansifer. Explaining type errors in polymorphic languages. ACM Letters on Programming Languages and Systems, 2(4):17-30, March 1993. [ bib | .ps.gz ] |
| [55] | D. E. Bell and Leonard J. LaPadula. Secure computer systems: Unified exposition and Multics interpretation. Technical Report MTR-2997, The MITRE Corp., July 1975. [ bib | .pdf ] |
| [56] | Jeffrey M. Bell, Françoise Bellegarde, and James Hook. Type-driven defunctionalization. In ACM International Conference on Functional Programming (ICFP), August 1997. [ bib | http ] |
| [57] | Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn. Smallfoot: Modular automatic assertion checking with separation logic. In International Symposium on Formal Methods for Components and Objects, volume 4111 of Lecture Notes in Computer Science, pages 115-137. Springer Verlag, November 2005. [ bib | .pdf ] |
| [58] | Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn. Symbolic execution with separation logic. In Asian Symposium on Programming Languages and Systems (APLAS), volume 3780 of Lecture Notes in Computer Science, pages 52-68. Springer Verlag, 2005. [ bib ] |
| [59] | Josh Berdine and Peter W. O'Hearn. Strong update, disposal, and encapsulation in bunched typing. In Mathematical Foundations of Programming Semantics, volume 158 of Electronic Notes in Theoretical Computer Science, pages 81-98. Elsevier Science, May 2006. [ bib | .pdf ] |
| [60] | Martin Berger, Kohei Honda, and Nobuko Yoshida. A logical analysis of aliasing in imperative higher-order functions. In ACM International Conference on Functional Programming (ICFP), pages 280-293, September 2005. [ bib | http ] |
| [61] | K. Bernstein and E. W. Stark. Debugging type errors. November 1995. [ bib | .ps.gz ] |
| [62] | Bernard Berthomieu and Camille le Moniès de Sagazan. A calculus of tagged types, with applications to process languages. In Workshop on Types for Program Analysis, pages 1-15, May 1995. [ bib | .ps.gz ] |
| [63] | Frédéric Besson, Thomas de Grenier de Latour, and Thomas Jensen. Secure calling contexts for stack inspection. In International ACM Conference on Principles and Practice of Declarative Programming (PPDP), pages 76-87, October 2002. [ bib | .pdf ] |
| [64] | Frédéric Besson, Thomas P. Jensen, Daniel Le Métayer, and Tommy Thorn. Model checking security properties of control flow graphs. Journal of Computer Security, 9(3):217-250, 2001. [ bib | .pdf ] |
| [65] | Achyutram Bhamidipaty and Todd A. Proebsting. Very fast YACC-compatible parsers (for very little effort). Software - Practice & Experience, 28(2):181-190, February 1998. [ bib | .ps ] |
| [66] | Girish Bhat and Rance Cleaveland. Efficient local model-checking for fragments of the modal μ-calculus. In International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), volume 1055 of Lecture Notes in Computer Science, pages 107-126. Springer Verlag, March 1996. [ bib | .ps.gz ] |
| [67] | Armin Biere, Alessandro Cimatti, Edmund Clarke, and Yunshan Zhu. Symbolic model checking without BDDs. In International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), volume 1579 of Lecture Notes in Computer Science, pages 193-207. Springer Verlag, March 1999. [ bib | .pdf ] |
| [68] | Bodil Biering, Lars Birkedal, and Noah Torp-Smith. BI hyperdoctrines and higher-order separation logic. In European Symposium on Programming (ESOP), volume 3444 of Lecture Notes in Computer Science, pages 233-247. Springer Verlag, April 2005. [ bib | .pdf ] |
| [69] | Richard Bird and Lambert Meertens. Nested datatypes. In International Conference on Mathematics of Program Construction (MPC), volume 1422 of Lecture Notes in Computer Science, pages 52-67. Springer Verlag, 1998. [ bib | .ps ] |
| [70] | Richard Bird and Ross Paterson. de Bruijn notation as a nested datatype. Journal of Functional Programming, 9(1):77-91, January 1999. [ bib | http ] |
| [71] | Lars Birkedal, Nick Rothwell, Mads Tofte, and David N. Turner. The ML kit (version 1). Technical Report DIKU 93/14, Department of Computer Science, University of Copenhagen, 1993. [ bib | http ] |
| [72] | Lars Birkedal and Mads Tofte. A constraint-based region inference algorithm. Theoretical Computer Science, 258:299-392, 2001. [ bib | .ps.gz ] |
| [73] | Lars Birkedal, Noah Torp-Smith, and Hongseok Yang. Semantics of separation-logic typing and higher-order frame rules for Algol-like languages. Logical Methods in Computer Science, 2(5), November 2006. [ bib | http ] |
| [74] | Andrew D. Birrell. An introduction to programming with C# threads. Manuscript, 2003. [ bib | .pdf ] |
| [75] | Sandip K. Biswas. Dynamic slicing in higher-order programming languages. PhD thesis, University of Pennsylvania, August 1997. [ bib ] |
| [76] | Chiara Bodei, Pierpaolo Degano, Flemming Nielson, and Hanne Riis Nielson. Static analysis of processes for no read-up and no write-down. In International Conference on Foundations of Software Science and Computation Structures (FOSSACS), volume 1578 of Lecture Notes in Computer Science, pages 120-134. Springer Verlag, March 1999. [ bib | .ps ] |
| [77] | Daniel Bonniot. Type-checking multi-methods in ML (a modular approach). In Workshop on Foundations of Object-Oriented Languages (FOOL), January 2002. [ bib | .ps ] |
| [78] | Urban Boquist. Code optimisation techniques for lazy functional languages. PhD thesis, Chalmers University of Technology, April 1999. [ bib | .ps.gz ] |
| [79] | Michele Boreale and Davide Sangiorgi. A fully abstract semantics for causality in the π-calculus. Acta Informatica, 35(5):353-400, May 1998. [ bib | .pdf ] |
| [80] | Richard Bornat. Proving pointer programs in Hoare logic. In International Conference on Mathematics of Program Construction (MPC), volume 1837 of Lecture Notes in Computer Science, pages 102-126. Springer Verlag, 2000. [ bib | .pdf ] |
| [81] | Richard Bornat, Cristiano Calcagno, Peter O'Hearn, and Matthew Parkinson. Permission accounting in separation logic. In ACM Symposium on Principles of Programming Languages (POPL), pages 259-270, January 2005. [ bib | .pdf ] |
| [82] | Gérard Boudol and Ilaria Castellani. Non-interference for concurrent programs and thread systems. To appear, September 2001. [ bib | .ps.gz ] |
| [83] | Sylvain Boulmé. Intuitionistic refinement calculus. In International Conference on Typed Lambda Calculi and Applications (TLCA), volume 4583 of Lecture Notes in Computer Science, pages 54-69. Springer Verlag, June 2007. [ bib | .pdf ] |
| [84] | François Bourdoncle and Stephan Merz. On the integration of functional programming, class-based object-oriented programming, and multi-methods. Research Report 26, Centre de Mathématiques Appliquées, Ecole des Mines de Paris, March 1996. [ bib | .html ] |
| [85] | François Bourdoncle and Stephan Merz. Type checking higher-order polymorphic multi-methods. In ACM Symposium on Principles of Programming Languages (POPL), pages 302-315, January 1997. [ bib | .html ] |
| [86] | Chandrasekhar Boyapati, Barbara Liskov, and Liuba Shrira. Ownership types for object encapsulation. In ACM Symposium on Principles of Programming Languages (POPL), pages 213-223, January 2003. [ bib | .pdf ] |
| [87] | John Tang Boyland and William Retert. Connecting effects and uniqueness with adoption. In ACM Symposium on Principles of Programming Languages (POPL), pages 283-295, January 2005. [ bib | .pdf ] |
| [88] | Gilad Bracha and William Cook. Mixin-based inheritance. In ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 303-311, 1990. [ bib | .ps ] |
| [89] | Gilad Bracha and Gary Lindstrom. Modularity meets inheritance. Technical Report UUCS-91-017, University of Utah, October 1991. [ bib | .ps ] |
| [90] | Marc M. Brandis and Hanspeter Mössenböck. Single-pass generation of static single-assignment form for structured languages. ACM Transactions on Programming Languages and Systems, 16(6):1684-1698, 1994. [ bib | .ps.gz ] |
| [91] | Michael Brandt and Fritz Henglein. Coinductive axiomatization of recursive type equality and subtyping. Fundamenta Informaticæ, 33:309-338, 1998. [ bib | .ps.gz ] |
| [92] | Val Breazu-Tannen, Thierry Coquand, Carl A. Gunter, and Andre Scedrov. Inheritance as implicit coercion. Information and Computation, 93(1):172-221, July 1991. [ bib | .pdf ] |
| [93] | Kim Bruce, Luca Cardelli, Giuseppe Castagna, The Hopkins Object Group, Gary T. Leavens, and Benjamin Pierce. On binary methods. Technical Report 95-08a, Department of Computer Science, Iowa State University, December 1995. [ bib | .ps.Z ] |
| [94] | Kim Bruce, Roberto Di Cosmo, and Giuseppe Longo. Provable isomorphisms of types. Mathematical Structures in Computer Science, 2(2):231-247, 1992. [ bib | .dvi ] |
| [95] | Kim B. Bruce, Luca Cardelli, and Benjamin C. Pierce. Comparing object encodings. Information and Computation, 155(1/2):108-133, November 1999. [ bib | .ps ] |
| [96] | Michele Bugliesi and Silvia Crafa. Object calculi for dynamic messages. In Workshop on Foundations of Object-Oriented Languages (FOOL), 1999. [ bib ] |
| [97] | Michele Bugliesi and Santiago M. Pericás-Geertsen. Type inference for variant object types. Information and Computation, 177(1):2-27, August 2002. [ bib | .ps.gz ] |
| [98] | Peter Buneman and Atsushi Ohori. Polymorphism and type inference in database programming. ACM Transactions on Database Systems, 21(1):30-76, 1996. [ bib | .pdf ] |
| [99] | Lilian Burdy, Yoonsik Cheon, David Cok, Michael Ernst, Joe Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll. An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer, 7(3):212-232, June 2005. [ bib | .pdf ] |
| [100] | R. M. Burstall, D. B. MacQueen, and D. T. Sannella. HOPE: An experimental applicative language. In ACM Symposium on Lisp and Functional Programming (LFP), pages 136-143, 1980. [ bib | http ] |
| [101] | Cristiano Calcagno, Simon Helsen, and Peter Thiemann. Syntactic type soundness results for the region calculus. Information and Computation, 173(2):199-221, 2002. [ bib | .pdf ] |
| [102] | Cristiano Calcagno, Eugenio Moggi, and Tim Sheard. Closed types for a safe imperative MetaML. Journal of Functional Programming, 13(3):545-571, May 2003. [ bib | http ] |
| [103] | Cristiano Calcagno, Eugenio Moggi, and Walid Taha. ML-like inference for classifiers. In European Symposium on Programming (ESOP), volume 2986 of Lecture Notes in Computer Science, pages 79-93. Springer Verlag, 2004. [ bib | .pdf ] |
| [104] | Luca Cardelli. Basic polymorphic typechecking. Science of Computer Programming, 8(2):147-172, 1987. [ bib | .pdf ] |
| [105] | Luca Cardelli. A semantics of multiple inheritance. Information and Computation, 76(2/3):138-164, February 1988. [ bib | .pdf ] |
| [106] | Luca Cardelli. Typeful programming. In Formal Description of Programming Concepts, IFIP State of the Art Reports Series. Springer Verlag, February 1989. [ bib | .pdf ] |
| [107] | Luca Cardelli. The Quest language and system, 1991. [ bib | .pdf ] |
| [108] | Luca Cardelli. Type systems. In Allen B. Tucker, editor, The Computer Science and Engineering Handbook, pages 2208-2236. CRC Press, 1997. [ bib | .pdf ] |
| [109] | Luca Cardelli and Giuseppe Longo. A semantic basis for Quest. Journal of Functional Programming, 1(4):417-458, October 1991. [ bib | .pdf ] |
| [110] | Luca Cardelli, Florian Matthes, and Martín Abadi. Extensible syntax with lexical scoping. Research Report 121, Digital Equipment Corporation, Systems Research Center, February 1994. [ bib | .ps.gz ] |
| [111] | Luca Cardelli and John Mitchell. Operations on records. In Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design. MIT Press, 1994. [ bib | .pdf ] |
| [112] | Luca Cardelli and Peter Wegner. On understanding types, data abstraction, and polymorphism. ACM Computing Surveys, 17(4):471-522, December 1985. [ bib | .pdf ] |
| [113] | Felice Cardone. A coinductive completeness proof for the equivalence of recursive types. Theoretical Computer Science, 275(1-2):575-587, 2002. [ bib | http ] |
| [114] | 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 European Symposium on Programming (ESOP), Lecture Notes in Computer Science. Springer Verlag, 2004. [ bib | .pdf ] |
| [115] | Sébastien Carlier and J. B. Wells. Type inference with expansion variables and intersection types in System E and an exact correspondence with β-reduction. Technical Report HW-MACS-TR-0012, Heriot-Watt University, January 2004. [ bib | .pdf ] |
| [116] | Robert Cartwright. Notes on object-oriented program design, January 2000. [ bib | http ] |
| [117] | Giuseppe Castagna. F<=& : integrating parametric and “ad hoc” second order polymorphism. In International Workshop on Database Programming Languages, Workshops in Computing. Springer Verlag, September 1993. [ bib ] |
| [118] | Giuseppe Castagna. Covariance and contravariance: Conflict without a cause. ACM Transactions on Programming Languages and Systems, 17(3):431-447, May 1995. [ bib | .ps.Z ] |
| [119] | Henry Cejtin, Matthew Fluet, Suresh Jagannathan, and Stephen Weeks. The MLton compiler. [ bib | http ] |
| [120] | Henry Cejtin, Suresh Jagannathan, and Stephen Weeks. Flow-directed closure conversion for typed languages. In European Symposium on Programming (ESOP), volume 1782 of Lecture Notes in Computer Science, pages 56-71. Springer Verlag, March 2000. [ bib | .ps.gz ] |
| [121] | Craig Chambers and Gary T. Leavens. BeCecil, a core object-oriented language with block structure and multimethods: Semantics and typing. Technical Report UW-CSE-96-12-02, University of Washington, December 1996. [ bib | .ps.gz ] |
| [122] | Arthur Charguéraud and François Pottier. Functional translation of a calculus of capabilities. Submitted, November 2007. [ bib | .pdf ] |
| [123] | Chih-Ping Chen and Paul Hudak. Rolling your own mutable ADT-a connection between linear types and monads. In ACM Symposium on Principles of Programming Languages (POPL), pages 54-66, January 1997. [ bib | .ps ] |
| [124] | Chiyan Chen, Rui Shi, and Hongwei Xi. A typeful approach to object-oriented programming with multiple inheritance. In International Workshop on Practical Aspects of Declarative Languages (PADL), volume 3057 of Lecture Notes in Computer Science. Springer Verlag, June 2004. [ bib | .pdf ] |
| [125] | Chiyan Chen and Hongwei Xi. Meta-programming through typeful code representation. In ACM International Conference on Functional Programming (ICFP), pages 275-286, August 2003. [ bib | .pdf ] |
| [126] | Chiyan Chen and Hongwei Xi. Combining programming with theorem proving. In ACM International Conference on Functional Programming (ICFP), September 2005. [ bib | .pdf ] |
| [127] | James Cheney. Scrap your nameplate. In ACM International Conference on Functional Programming (ICFP), September 2005. [ bib | .pdf ] |
| [128] | James Cheney and Ralf Hinze. A lightweight implementation of generics and dynamics. In Haskell workshop, 2002. [ bib | .pdf ] |
| [129] | James Cheney and Ralf Hinze. First-class phantom types. Technical Report 1901, Cornell University, 2003. [ bib | http ] |
| [130] | James Cheney and Christian Urban. αProlog: A logic programming language with names, binding and α-equivalence. In International Conference on Logic Programming (ICLP), volume 3132 of Lecture Notes in Computer Science, pages 269-283. Springer Verlag, September 2004. [ bib | .pdf ] |
| [131] | Olaf Chitil. Compositional explanation of types and algorithmic debugging of type errors. In ACM International Conference on Functional Programming (ICFP), pages 193-204, September 2001. [ bib | .ps.gz ] |
| [132] | Adam Chlipala. A certified type-preserving compiler from lambda calculus to assembly language. In ACM Conference on Programming Language Design and Implementation (PLDI), pages 54-65, June 2007. [ bib | .pdf ] |
| [133] | Venkatesh Choppella. Unification source-tracking with application to diagnosis of type inference. PhD thesis, Indiana University, August 2002. [ bib | http ] |
| [134] | Dave Clarke and Sophia Drossopoulou. Ownership, encapsulation and the disjointness of type and effect. In ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 292-310, November 2002. [ bib | .ps ] |
| [135] | David G. Clarke, John M. Potter, and James Noble. Ownership types for flexible alias protection. In ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 48-64, October 1998. [ bib | http ] |
| [136] | Edmund Clarke. Programming language constructs for which it is impossible to obtain good Hoare axiom systems. Journal of the ACM, 26(1):129-147, January 1979. [ bib | http ] |
| [137] | Rance Cleaveland and Bernhard Steffen. A linear-time model-checking algorithm for the alternation-free modal mu-calculus. In Computer Aided Verification, volume 575 of Lecture Notes in Computer Science, pages 48-58. Springer Verlag, 1991. [ bib | http ] |
| [138] | Dominique Clément, Joëlle Despeyroux, Thierry Despeyroux, and Gilles Kahn. A simple applicative language: Mini-ML. In ACM Symposium on Lisp and Functional Programming (LFP), pages 13-27, 1986. [ bib ] |
| [139] | John Clements and Matthias Felleisen. A tail-recursive semantics for stack inspections. In European Symposium on Programming (ESOP), volume 2618 of Lecture Notes in Computer Science, pages 22-37. Springer Verlag, April 2003. [ bib | .ps.gz ] |
| [140] | Dario Colazzo and Giorgio Ghelli. Subtyping recursive types in Kernel Fun. In IEEE Symposium on Logic in Computer Science (LICS), pages 137-146, July 1999. [ bib ] |
| [141] | Gregory D. Collins and Zhong Shao. Intensional analysis of higher-kinded recursive types. Technical Report YALEU/DCS/TR-1240, Yale University, 2002. [ bib | .pdf ] |
| [142] | Alain Colmerauer. Equations and inequations on finite and infinite trees. In International Conference on Fifth Generation Computer Systems (FGCS), pages 85-99, November 1984. [ bib ] |
| [143] | Hubert Comon. Constraints in term algebras (short survey). In International Conference on Algebraic Methodology and Software Technology (AMAST), Workshops in Computing. Springer Verlag, 1993. [ bib | .ps ] |
| [144] | Hubert Comon and Pierre Lescanne. Equational problems and disunification. Journal of Symbolic Computation, 7:371-425, 1989. [ bib | .pdf ] |
| [145] | Sylvain Conchon and Evelyne Contejean. The Ergo automatic theorem prover, 2006. http://ergo.lri.fr/. [ bib | http ] |
| [146] | Sylvain Conchon and Fabrice Le Fessant. Jocaml: Mobile agents for Objective-Caml. In International Symposium on Agent Systems and Applications and International Symposium on Mobile Agents (ASA/MA), pages 22-29, October 1999. [ bib | .ps.gz ] |
| [147] | Sylvain Conchon and François Pottier. JOIN(X): Constraint-based type inference for the join-calculus. In European Symposium on Programming (ESOP), volume 2028 of Lecture Notes in Computer Science, pages 221-236. Springer Verlag, April 2001. [ bib | .ps.gz ] |
| [148] | Jeffrey Considine. Efficient hash-consing of recursive types. Technical Report 2000-006, Boston University, January 2000. [ bib | .pdf ] |
| [149] | Mario Coppo and Mariangiola Dezani-Ciancaglini. An extension of the basic functionality theory for the λ-calculus. Notre Dame J. Formal Logic, 21(4):685-693, 1980. [ bib ] |
| [150] | Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. Introduction à l'algorithmique: Cours et exercices. Sciences Sup. Dunod, 2002. [ bib ] |
| [151] | Bruno Courcelle. Fundamental properties of infinite trees. Theoretical Computer Science, 25(2):95-169, March 1983. [ bib ] |
| [152] | Patrick Cousot. Methods and logics for proving programs. In Formal Models and Semantics, volume B of Handbook of Theoretical Computer Science, chapter 15, pages 841-993. Elsevier Science, 1990. [ bib | .pdf.gz ] |
| [153] | Patrick Cousot and Radhia Cousot. Formal language, grammar and set-constraint-based program analysis by abstract interpretation. In Conference on Functional Programming Languages and Computer Architecture (FPCA), pages 170-181. ACM Press, 1995. [ bib ] |
| [154] | Erik Crank and Matthias Felleisen. Parameter-passing and the lambda calculus. In ACM Symposium on Principles of Programming Languages (POPL), pages 233-244, January 1991. [ bib | .ps.gz ] |
| [155] | Karl Crary. Type-theoretic methodology for practical programming languages. PhD thesis, Cornell University, August 1998. [ bib | .ps.gz ] |
| [156] | Karl Crary. Simple, efficient object encoding using intersection types. Technical Report CMU-CS-99-100, Carnegie Mellon University, 1999. [ bib | .ps.gz ] |
| [157] | Karl Crary, David Walker, and Greg Morrisett. Typed memory management in a calculus of capabilities. In ACM Symposium on Principles of Programming Languages (POPL), pages 262-275, January 1999. [ bib | .pdf ] |
| [158] | Karl Crary and Stephanie Weirich. Flexible type analysis. In ACM International Conference on Functional Programming (ICFP), pages 233-248, 1999. [ bib | .ps.gz ] |
| [159] | Karl Crary and Stephanie Weirich. Resource bound certification. In ACM Symposium on Principles of Programming Languages (POPL), pages 184-198, January 2000. [ bib | .pdf ] |
| [160] | Karl Crary, Stephanie Weirich, and Greg Morrisett. Intensional polymorphism in type-erasure semantics. In ACM International Conference on Functional Programming (ICFP), pages 301-313, September 1998. [ bib | .ps ] |
| [161] | Karl Crary, Stephanie Weirich, and Greg Morrisett. Intensional polymorphism in type erasure semantics. Journal of Functional Programming, 12(6):567-600, November 2002. [ bib | .ps ] |
| [162] | Pavel Curtis. Constrained quantification in polymorphic type analysis. PhD thesis, Cornell University, February 1990. [ bib | .ps.gz ] |
| [163] | Luis Damas. Type assignment in programming languages. PhD thesis, University of Edinburgh, 1985. [ bib ] |
| [164] | Luis Damas and Robin Milner. Principal type-schemes for functional programs. In ACM Symposium on Principles of Programming Languages (POPL), pages 207-212, 1982. [ bib | http ] |
| [165] | Werner Damm and Bernhard Josko. A sound and relatively* complete axiomatization of Clarke's language L4. In Logic of Programs, volume 164 of Lecture Notes in Computer Science, pages 161-175. Springer Verlag, 1983. [ bib | http ] |
| [166] | Nils Anders Danielsson. Lightweight semiformal time complexity analysis for purely functional data structures. In ACM Symposium on Principles of Programming Languages (POPL), January 2008. [ bib | .pdf ] |
| [167] | Nils Anders Danielsson, John Hughes, Patrik Jansson, and Jeremy Gibbons. Fast and loose reasoning is morally correct. In ACM Symposium on Principles of Programming Languages (POPL), pages 206-217, January 2006. [ bib | .pdf ] |
| [168] | Olivier Danvy. Functional unparsing. Technical Report RS-98-12, BRICS, May 1998. [ bib | http ] |
| [169] | Olivier Danvy. Functional unparsing. Journal of Functional Programming, 8(6):621-625, November 1998. [ bib | http ] |
| [170] | Olivier Danvy and Lasse R. Nielsen. Defunctionalization at work. Technical Report RS-01-23, BRICS, June 2001. [ bib | http ] |
| [171] | Olivier Danvy and Lasse R. Nielsen. Defunctionalization at work. In International ACM Conference on Principles and Practice of Declarative Programming (PPDP), pages 162-174, September 2001. [ bib | http ] |
| [172] | Thi Bich Hanh Dao. Résolution de contraintes du premier ordre dans la théorie des arbres finis ou infinis. PhD thesis, Université de la Méditerranée, December 2000. [ bib | .ps.gz ] |
| [173] | Rowan Davies. Practical refinement-type checking. Technical Report CMU-CS-05-110, School of Computer Science, Carnegie Mellon University, May 2005. [ bib | .pdf ] |
| [174] | Rowan Davies and Frank Pfenning. Intersection types and computational effects. In ACM International Conference on Functional Programming (ICFP), pages 198-208, September 2000. [ bib | .pdf ] |
| [175] | Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem-proving. Communications of the ACM, 5(7):394-397, 1962. [ bib | http ] |
| [176] | Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM, 7(3):201-215, 1960. [ bib | http ] |
| [177] | Nicolaas G. de Bruijn. Lambda-calculus notation with nameless dummies: a tool for automatic formula manipulation with application to the Church-Rosser theorem. Indag. Math., 34(5):381-392, 1972. [ bib ] |
| [178] | Edsko de Vries, Rinus Plasmeijer, and David Abrahamson. Uniqueness typing redefined. In Implementation of Functional Languages (IFL), volume 4449 of Lecture Notes in Computer Science, pages 181-198. Springer Verlag, 2006. [ bib | .pdf ] |
| [179] | Edsko de Vries, Rinus Plasmeijer, and David Abrahamson. Equality based uniqueness typing. In Trends in Functional Programming (TFP), 2007. [ bib | .pdf ] |
| [180] | M. Debbabi, E. Giasson, B. Ktari, F. Michaud, and N. Tawbi. Secure self-certified COTS. In IEEE International Workshop on Enterprise Security (WETICE'00), June 2000. [ bib | .pdf ] |
| [181] | Robert DeLine and Manuel Fähndrich. Enforcing high-level protocols in low-level software. In ACM Conference on Programming Language Design and Implementation (PLDI), pages 59-69, June 2001. [ bib | .pdf ] |
| [182] | Dorothy E. Denning. Cryptography and data security. Addison-Wesley, 1982. [ bib ] |
| [183] | Dorothy E. Denning and Peter J. Denning. Certification of programs for secure information flow. Communications of the ACM, 20(7):504-513, July 1977. [ bib ] |
| [184] | Greg Dennis, Felix Change, and Daniel Jackson. Modular verification of code with SAT. In International Symposium on Software Testing and Analysis (ISSTA), July 2006. [ bib | .pdf ] |
| [185] | Frank DeRemer and Thomas Pennello. Efficient computation of LALR(1) look-ahead sets. ACM Transactions on Programming Languages and Systems, 4(4):615-649, 1982. [ bib | http ] |
| [186] | David Detlefs, Greg Nelson, and James B. Saxe. Simplify: a theorem prover for program checking. Journal of the ACM, 52(3):365-473, 2005. [ bib | http ] |
| [187] | David L. Detlefs, K. Rustan M. Leino, and Greg Nelson. Wrestling with rep exposure. Research Report 156, SRC, July 1998. [ bib | .pdf ] |
| [188] | David L. Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe. Extended static checking. Research Report 159, Compaq SRC, December 1998. [ bib | .pdf ] |
| [189] | Roberto Di Cosmo. Deciding type isomorphisms in a type assignment framework. Journal of Functional Programming, 3(3):485-525, 1993. [ bib | .dvi ] |
| [190] | Roberto Di Cosmo. Isomorphisms of types: from λ-calculus to information retrieval and language design. Progress in Theoretical Computer Science. Birkhauser, 1995. [ bib | .html ] |
| [191] | E. W. Dijkstra. A note on two problems in connection with graphs. Numerische Mathematik, 1:269-271, 1959. [ bib ] |
| [192] | Allyn Dimock. Type- and flow-directed compilation for specialized data representations. PhD thesis, Harvard University, January 2002. [ bib | .ps.gz ] |
| [193] | Allyn Dimock, Ian Westmacott, Robert Muller, Franklyn Turbak, and J. B. Wells. Functioning without closure: Type-safe customized function representations for standard ML. In ACM International Conference on Functional Programming (ICFP), September 2001. [ bib | .ps ] |
| [194] | Charles Donnelly and Richard Stallman. Bison, September 2005. [ bib | http ] |
| [195] | Kevin Donnelly and Hongwei Xi. Combining higher-order abstract syntax with first-order abstract syntax in ATS. In ACM Workshop on Mechanized Reasoning about Languages with Variable Binding, pages 58-63, 2005. [ bib | .pdf ] |
| [196] | Gilles Dowek. Higher-order unification and matching. In J. Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, pages 1009-1062. Elsevier Science, 2001. [ bib | .ps ] |
| [197] | Gilles Dowek, Thérèse Hardin, and Claude Kirchner. Higher order unification via explicit substitutions. Research Report 2709, INRIA, November 1995. [ bib | .html ] |
| [198] | Gilles Dowek, Thérèse Hardin, Claude Kirchner, and Frank Pfenning. Unification via explicit substitutions: the case of higher-order patterns. Research Report 3591, INRIA, December 1998. [ bib | .html ] |
| [199] | Peter J. Downey, Ravi Sethi, and Robert Endre Tarjan. Variations on the common subexpression problem. Journal of the ACM, 27(4):758-771, October 1980. [ bib | http ] |
| [200] | Catherine Dubois and Valérie Ménissier-Morain. Typage de ML: Spécification et preuve en Coq. In Actes du GDR Programmation, November 1997. [ bib | .ps.gz ] |
| [201] | Catherine Dubois and Valérie Ménissier-Morain. Certification of a type inference tool for ML: Damas-Milner within Coq. Journal of Automated Reasoning, 23(3-4):319-346, November 1999. [ bib | .ps.gz ] |
| [202] | Dominic Duggan and Frederick Bent. Explaining type inference. Science of Computer Programming, 27(1), June 1996. [ bib ] |
| [203] | Dirk Dussart, Fritz Henglein, and Christian Mossin. Polymorphic recursion and subtype qualifications: Polymorphic binding-time analysis in polynomial time. In Static Analysis Symposium (SAS), volume 983 of Lecture Notes in Computer Science, pages 118-135. Springer Verlag, September 1995. [ bib | .dvi.gz ] |
| [204] | Jonathan Eifrig, Scott Smith, and Valery Trifonov. Sound polymorphic type inference for objects. ACM SIGPLAN Notices, 30(10):169-184, 1995. [ bib | .ps.gz ] |
| [205] | Jonathan Eifrig, Scott Smith, and Valery Trifonov. Type inference for recursively constrained types and its application to OOP. In Mathematical Foundations of Programming Semantics, volume 1 of Electronic Notes in Theoretical Computer Science. Elsevier Science, 1995. [ bib | .ps.gz ] |
| [206] | Martin Emms and Hans Leiß. Extending the type checker for SML by polymorphic recursion - A correctness proof. Technical Report 96-101, Centrum für Informations- und Sprachverarbeitung, Universität München, 1996. [ bib | .ps.gz ] |
| [207] | Úlfar Erlingsson and Fred B. Schneider. SASI enforcement of security policies: a retrospective. In New Security Paradigms Workshop, pages 87-95, September 1999. [ bib | .ps ] |
| [208] | Úlfar Erlingsson and Fred B. Schneider. IRM enforcement of Java stack inspection. In IEEE Symposium on Security and Privacy (S&P), pages 246-255, May 2000. [ bib | http ] |
| [209] | Karl-Filip Faxén. A static semantics for Haskell. Journal of Functional Programming, 12(4-5):295-357, July 2002. [ bib | .ps.gz ] |
| [210] | Christian Fecht and Helmut Seidl. A faster solver for general systems of equations. Science of Computer Programming, 35(2-3):137-162, 1999. [ bib | .ps.gz ] |
| [211] | J. S. Fenton. Information protection systems. PhD thesis, University of Cambridge, 1973. [ bib ] |
| [212] | J. S. Fenton. Memoryless subsystems. Computer Journal, 17(2):143-147, May 1974. [ bib ] |
| [213] | John Field and Tim Teitelbaum. Incremental reduction in the lambda calculus. In ACM Symposium on Lisp and Functional Programming (LFP), pages 307-322, 1990. [ bib ] |
| [214] | Andrzej Filinski. Representing layered monads. In ACM Symposium on Principles of Programming Languages (POPL), pages 175-188, January 1999. [ bib | .ps.gz ] |
| [215] | Jean-Christophe Filliâtre. Backtracking iterators. In ACM Workshop on ML, September 2006. [ bib | .ps.gz ] |
| [216] | Jean-Christophe Filliâtre. Verification of non-functional programs using interpretations in type theory. Journal of Functional Programming, 13(4):709-745, July 2003. [ bib | .ps.gz ] |
| [217] | Jean-Christophe Filliâtre. Why: a multi-language multi-prover verification tool. Research Report 1366, LRI, Université Paris Sud, March 2003. [ bib | .ps.gz ] |
| [218] | Jean-Christophe Filliâtre. Formal proof of a program: Find. Science of Computer Programming, 64:332-240, 2006. [ bib | .ps.gz ] |
| [219] | Jean-Christophe Filliâtre and Pierre Letouzey. Functors for proofs and programs. In European Symposium on Programming (ESOP), volume 2986 of Lecture Notes in Computer Science, pages 370-384. Springer Verlag, March 2004. [ bib | .ps.gz ] |
| [220] | Jean-Christophe Filliâtre and Claude Marché. Multi-prover verification of C programs. In International Conference on Formal Engineering Methods (ICFEM), volume 3308 of Lecture Notes in Computer Science, pages 15-29. Springer Verlag, November 2004. [ bib | .ps.gz ] |
| [221] | Jean-Christophe Filliâtre and Claude Marché. The Why/Krakatoa/Caduceus platform for deductive program verification. In Computer Aided Verification, volume 4590 of Lecture Notes in Computer Science, pages 173-177. Springer Verlag, July 2007. [ bib | .pdf ] |
| [222] | Robert Bruce Findler and Matthias Felleisen. Contracts for higher-order functions. In ACM International Conference on Functional Programming (ICFP), pages 48-59, October 2002. [ bib | .pdf ] |
| [223] | Adam Fischbach and John Hannan. Specification and correctness of lambda lifting. Journal of Functional Programming, 13(3):509-543, May 2003. [ bib | http ] |
| [224] | Kathleen Fisher and John C. Mitchell. On the relationship between classes, objects and data abstraction. Theory and Practice of Object Systems, 4(1):3-25, 1998. [ bib | .ps ] |
| [225] | Cormac Flanagan. Effective static debugging via componential set-based analysis. PhD thesis, Rice University, May 1997. [ bib | .ps.gz ] |
| [226] | Cormac Flanagan and Matthias Felleisen. Modular and polymorphic set-based analysis: Theory and practice. Technical Report TR96-266, Rice University, November 1996. [ bib | .ps.gz ] |
| [227] | Cormac Flanagan and Matthias Felleisen. Componential set-based analysis. In ACM Conference on Programming Language Design and Implementation (PLDI), pages 235-248, 1997. [ bib | .ps.gz ] |
| [228] | Cormac Flanagan, Matthew Flatt, Shriram Krishnamurthi, Stephanie Weirich, and Matthias Felleisen. Catching bugs in the web of program invariants. In ACM Conference on Programming Language Design and Implementation (PLDI), 1996. [ bib | .ps.gz ] |
| [229] | Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata. Extended static checking for Java. In ACM Conference on Programming Language Design and Implementation (PLDI), pages 234-245, 2002. [ bib | .ps ] |
| [230] | Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The essence of compiling with continuations. In ACM Conference on Programming Language Design and Implementation (PLDI), pages 237-247, 1993. [ bib | .ps.gz ] |
| [231] | Cormac Flanagan and James B. Saxe. Avoiding exponential explosion: generating compact verification conditions. In ACM Symposium on Principles of Programming Languages (POPL), pages 193-205, 2001. [ bib | .ps ] |
| [232] | R. W. Floyd. Assigning meanings to programs. In Mathematical Aspects of Computer Science, volume 19 of Proceedings of Symposia in Applied Mathematics, pages 19-32. American Mathematical Society, 1967. [ bib ] |
| [233] | Matthew Fluet. Monadic and substructural type systems for region-based memory management. PhD thesis, Cornell University, January 2007. [ bib | .pdf ] |
| [234] | Matthew Fluet and Greg Morrisett. Monadic regions. Journal of Functional Programming, 16(4-5):485-545, 2006. [ bib | .pdf ] |
| [235] | Matthew Fluet, Greg Morrisett, and Amal Ahmed. Linear regions are all you need. In European Symposium on Programming (ESOP), volume 3924 of Lecture Notes in Computer Science, pages 7-21. Springer Verlag, March 2006. [ bib | .pdf ] |
| [236] | Matthew Fluet and Riccardo Pucella. Phantom types and subtyping. In IFIP International Conference on Theoretical Computer Science (TCS), pages 448-460, August 2002. [ bib | http ] |
| [237] | Matthew Fluet and Riccardo Pucella. Phantom types and subtyping. In IFIP International Conference on Theoretical Computer Science (TCS), volume 223 of IFIP Conference Proceedings, pages 448-460. Kluwer, August 2002. [ bib | .ps ] |
| [238] | Matthew Fluet and Riccardo Pucella. Practical datatype specializations with phantom types and recursion schemes. In ACM Workshop on ML, Electronic Notes in Theoretical Computer Science, September 2005. [ bib | .pdf ] |
| [239] | Riccardo Focardi and Roberto Gorrieri. A classification of security properties for process algebras. Journal of Computer Security, 3(1):5-33, 1995. [ bib | .ps.gz ] |
| [240] | Jeffrey S. Foster and Alex Aiken. Checking programmer-specified non-aliasing. Technical Report UCB//CSD-01-1160, University of California, Berkeley, October 2001. [ bib | .pdf ] |
| [241] | Jeffrey S. Foster, Tachio Terauchi, and Alex Aiken. Flow-sensitive type qualifiers. In ACM Conference on Programming Language Design and Implementation (PLDI), pages 1-12, June 2002. [ bib | .pdf ] |
| [242] | Cédric Fournet and Georges Gonthier. The reflexive chemical abstract machine and the join-calculus. In ACM Symposium on Principles of Programming Languages (POPL), pages 372-385, 1996. [ bib | .ps ] |
| [243] | Cédric Fournet and Andrew D. Gordon. Stack inspection: Theory and variants. In ACM Symposium on Principles of Programming Languages (POPL), pages 307-318, January 2002. [ bib | .ps ] |
| [244] | Cédric Fournet and Andrew D. Gordon. Stack inspection: Theory and variants. ACM Transactions on Programming Languages and Systems, 25(3):360-399, May 2003. [ bib | http ] |
| [245] | Cédric Fournet, Cosimo Laneve, Luc Maranget, and Didier Rémy. Inheritance in the join calculus. 2000. [ bib | http ] |
| [246] | Cédric Fournet, Luc Maranget, Cosimo Laneve, and Didier Rémy. Implicit typing à la ML for the join-calculus. In International Conference on Concurrency Theory (CONCUR), volume 1243 of Lecture Notes in Computer Science, pages 196-212. Springer Verlag, 1997. [ bib | .ps.gz ] |
| [247] | Tim Freeman and Frank Pfenning. Refinement types for ML. In ACM Conference on Programming Language Design and Implementation (PLDI), pages 268-277, 1991. [ bib | .pdf ] |
| [248] | Alexandre Frey. Satisfying subtype inequalities in polynomial space. In Static Analysis Symposium (SAS), number 1302 in Lecture Notes in Computer Science, pages 265-277. Springer Verlag, September 1997. [ bib | .html ] |
| [249] | Alexandre Frey. Approche algébrique du typage d'un langage à la ML avec objets, sous-typage et multi-méthodes. PhD thesis, École des Mines de Paris, June 2004. [ bib | .pdf ] |
| [250] | You-Chin Fuh and Prateek Mishra. Type inference with subtypes. In European Symposium on Programming (ESOP), volume 300 of Lecture Notes in Computer Science, pages 94-114. Springer Verlag, 1988. [ bib | http ] |
| [251] | You-Chin Fuh and Prateek Mishra. Polymorphic subtype inference: Closing the theory-practice gap. In International Joint Conference on Theory and Practice of Software Development (TAPSOFT), volume 352 of Lecture Notes in Computer Science, pages 167-183. Springer Verlag, March 1989. [ bib | http ] |
| [252] | Jun Furuse. Extensional polymorphism by flow graph dispatching. In Asian Symposium on Programming Languages and Systems (APLAS), volume 2895 of Lecture Notes in Computer Science. Springer Verlag, November 2003. [ bib | .ps.gz ] |
| [253] | Jun P. Furuse and Jacques Garrigue. A label-selective lambda-calculus with optional arguments and its compilation method. RIMS Preprint 1041, Kyoto University, October 1995. [ bib | .pdf ] |
| [254] | Manuel Fähndrich. Bane: A library for scalable constraint-based program analysis. PhD thesis, University of California at Berkeley, 1999. [ bib | .pdf ] |
| [255] | Manuel Fähndrich, Mark Aiken, Chris Hawblitzel, Orion Hodson, Galen Hunt, James R. Larus, and Steven Levi. Language support for fast and reliable message-based communication in Singularity OS. In EuroSys, pages 177-190, 2006. [ bib | .pdf ] |
| [256] | Manuel Fähndrich and Robert DeLine. Adoption and focus: practical linear types for imperative programming. In ACM Conference on Programming Language Design and Implementation (PLDI), pages 13-24, June 2002. [ bib | .pdf ] |
| [257] | Manuel Fähndrich, Jeffrey S. Foster, Zhendong Su, and Alexander S. Aiken. Partial online cycle elimination in inclusion constraint graphs. In ACM Conference on Programming Language Design and Implementation (PLDI), pages 85-96, June 1998. [ bib | .ps ] |
| [258] | Manuel Fähndrich and Rustan Leino. Heap monotonic typestates. In International Workshop on Alias Confinement and Ownership (IWACO), July 2003. [ bib | .pdf ] |
| [259] | Manuel Fähndrich, Jakob Rehof, and Manuvir Das. Scalable context-sensitive flow analysis using instantiation constraints. In ACM Conference on Programming Language Design and Implementation (PLDI), June 2000. [ bib | .ps ] |
| [260] | Murdoch J. Gabbay. A theory of inductive definitions with α-equivalence. PhD thesis, Cambridge University, 2001. [ bib | .pdf ] |
| [261] | Murdoch J. Gabbay. A general mathematics of names in syntax. Submitted for publication, March 2004. [ bib | .pdf ] |
| [262] | Murdoch J. Gabbay and Andrew M. Pitts. A new approach to abstract syntax with variable binding. Formal Aspects of Computing, 13(3-5):341-363, July 2002. [ bib | .pdf ] |
| [263] | Vladimir Gapeyev, Michael Levin, and Benjamin Pierce. Recursive subtyping revealed. Journal of Functional Programming, 12(6):511-548, 2003. [ bib | http ] |
| [264] | Michael R. Garey and David S. Johnson. Computers and intractability: A guide to the theory of NP-completeness. W. H. Freeman and Company, 1979. [ bib ] |
| [265] | Jacques Garrigue. Programming with polymorphic variants. In ACM Workshop on ML, September 1998. [ bib | .ps.gz ] |
| [266] | Jacques Garrigue. Code reuse through polymorphic variants. In Workshop on Foundations of Software Engineering, November 2000. [ bib | .ps.gz ] |
| [267] | Jacques Garrigue. Simple type inference for structural polymorphism. In Workshop on Foundations of Object-Oriented Languages (FOOL), January 2002. [ bib | .ps.gz ] |
| [268] | Jacques Garrigue. Relaxing the value restriction. Draft, August 2003. [ bib | .ps.gz ] |
| [269] | Jacques Garrigue and Didier Rémy. Extending ML with semi-explicit higher-order polymorphism. Information and Computation, 155(1):134-169, 1999. [ bib | .ps.gz ] |
| [270] | Benedict R. Gaster. Records, variants and qualified types. PhD thesis, University of Nottingham, July 1998. [ bib | .ps ] |
| [271] | Benedict R. Gaster and Mark P. Jones. A polymorphic type system for extensible records and variants. Technical Report NOTTCS-TR-96-3, Department of Computer Science, University of Nottingham, November 1996. [ bib | .html ] |
| [272] | Steven German, Edmund Clarke, and Joseph Halpern. Reasoning about procedures as parameters. In Logic of Programs, volume 164 of Lecture Notes in Computer Science, pages 206-220. Springer Verlag, 1983. [ bib | http ] |
| [273] | Alfons Geser, Jens Knoop, Gerald Lüttgen, Oliver Rüthing, and Bernhard Steffen. Chaotic fixed point iterations. MIP-Bericht 9403, Fakultät für Mathematik und Informatik, Universität Passau, 1994. [ bib | .html ] |
| [274] | Giorgio Ghelli. Divergence of F<= type checking. Theoretical Computer Science, 139(1-2):131-162, March 1995. [ bib | .ps.gz ] |
| [275] | David K. Gifford, Pierre Jouvelot, John M. Lucassen, and Mark A. Sheldon. FX-87 reference manual. Technical Report MIT/LCS/TR-407, Massachusetts Institute of Technology, January 1987. [ bib ] |
| [276] | David K. Gifford, Pierre Jouvelot, Mark A. Sheldon, and James W. O'Toole. Report on the FX-91 programming language. Technical Report MIT/LCS/TR-531, Massachusetts Institute of Technology, February 1992. [ bib | http ] |
| [277] | Jean-Yves Girard. Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur. Thèse d'état, Université Paris 7, June 1972. [ bib ] |
| [278] | Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-102, 1987. [ bib | .pdf ] |
| [279] | Neal Glew. Object closure conversion. In International Workshop on Higher Order Operational Techniques in Semantics (HOOTS), September 1999. [ bib | .ps.gz ] |
| [280] | Neal Glew. An efficient class and object encoding. In ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 311-324, October 2000. [ bib | .ps.gz ] |
| [281] | Neal Glew. A theory of second-order trees. In European Symposium on Programming (ESOP), volume 2305 of Lecture Notes in Computer Science, pages 147-161. Springer Verlag, April 2002. [ bib | .pdf ] |
| [282] | Andreas Goerdt. A Hoare calculus for functions defined by recursion on higher types. In Logic of Programs, volume 193 of Lecture Notes in Computer Science, pages 106-117. Springer Verlag, 1985. [ bib | http ] |
| [283] | Joseph Goguen and José Meseguer. Security policies and security models. In IEEE Symposium on Security and Privacy (S&P), pages 11-20, April 1982. [ bib ] |
| [284] | Li Gong, Gary Ellison, and Mary Dageforde. Inside Java 2 platform security, second edition. Addison-Wesley, 2003. [ bib | http ] |
| [285] | Li Gong, Marianne Mueller, Hemma Prafullchandra, and Roland Schemers. Going beyond the sandbox: An overview of the new security architecture in the Java Development Kit 1.2. In USENIX Symposium on Internet Technologies and Systems, pages 103-112, December 1997. [ bib | .ps ] |
| [286] | Li Gong and Roland Schemers. Implementing protection domains in the Java development kit 1.2. In Internet Society Symposium on Network and Distributed System Security, March 1998. [ bib | .pdf ] |
| [287] | Andrew D. Gordon and Tom Melham. Five axioms of alpha-conversion. In International Conference on Theorem Proving in Higher Order Logics (TPHOLs), volume 1125 of Lecture Notes in Computer Science, pages 173-191. Springer Verlag, August 1996. [ bib | .ps.gz ] |
| [288] | James Gosling, Bill Joy, Guy Steele, and Gilad Bracha. The Java language specification, second edition. Addison-Wesley, 2000. [ bib | http ] |
| [289] | Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, and Mooly Sagiv. Local reasoning for storable locks and threads. Technical Report MSR-TR-2007-39, Microsoft Research, September 2007. [ bib | .pdf ] |
| [290] | Jean Goubault. Inférence d'unités physiques en ML. In Journées Françaises des Langages Applicatifs, pages 3-20, 1994. [ bib ] |
| [291] | Jessica Gronski, Kenneth Knowles, Aaron Tomb, Stephen N. Freund, and Cormac Flanagan. Sage: Hybrid checking for flexible specifications. In Scheme and Functional Programming, September 2006. [ bib | .pdf ] |
| [292] | Dan Grossman. Quantified types in an imperative language. ACM Transactions on Programming Languages and Systems, 28(3):429-475, May 2006. [ bib | .pdf ] |
| [293] | Dan Grossman, Greg Morrisett, Trevor Jim, Michael Hicks, Yanling Wang, and James Cheney. Region-based memory management in Cyclone. In ACM Conference on Programming Language Design and Implementation (PLDI), pages 282-293, June 2002. [ bib | .pdf ] |
| [294] | Dick Grune and Ceriel J. H. Jacobs. Parsing techniques: a practical guide. Ellis Horwood, 1990. [ bib | .html ] |
| [295] | Jörgen Gustavsson and Josef Svenningsson. Constraint abstractions. In Symposium on Programs as Data Objects, volume 2053 of Lecture Notes in Computer Science. Springer Verlag, May 2001. [ bib | .ps ] |
| [296] | Juan Carlos Guzmán and Ascánder Suárez. An extended type system for exceptions. In ACM Workshop on ML and its Applications, number 2265 in INRIA Research Reports, pages 127-135. INRIA, June 1994. [ bib ] |
| [297] | Christian Haack and J. B. Wells. Type error slicing in implicitly typed, higher-order languages. In European Symposium on Programming (ESOP), volume 2618 of Lecture Notes in Computer Science. Springer Verlag, 2003. [ bib | .pdf ] |
| [298] | Cordelia Hall, Kevin Hammond, Simon Peyton Jones, and Philip Wadler. Type classes in Haskell. In European Symposium on Programming (ESOP), volume 788 of Lecture Notes in Computer Science, pages 241-256. Springer Verlag, April 1994. [ bib | .ps.gz ] |
| [299] | Cordelia Hall, Kevin Hammond, Simon Peyton Jones, and Philip Wadler. Type classes in Haskell. ACM Transactions on Programming Languages and Systems, 18(2):109-138, March 1996. [ bib | http ] |
| [300] | 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. [ bib | .pdf ] |
| [301] | Thomas Hallgren, James Hook, Mark P. Jones, and Richard Kieburtz. An overview of the Programatica toolset. High Confidence Software and Systems Conference (HCSS), 2004. [ bib | .pdf ] |
| [302] | Michael Hanus. Horn clause specifications with polymorphic types. PhD thesis, Fachbereich Informatik, Universität Dortmund, 1988. [ bib | .dvi.Z ] |
| [303] | Michael Hanus. Horn clause programs with polymorphic types: Semantics and resolution. In International Joint Conference on Theory and Practice of Software Development (TAPSOFT), volume 352 of Lecture Notes in Computer Science, pages 225-240. Springer Verlag, 1989. [ bib | .ps ] |
| [304] | Norm Hardy. The confused deputy (or why capabilities might have been invented). ACM Operating Systems Review, 22(4):36-38, October 1988. [ bib | .html ] |
| [305] | Bob Harper and Mark Lillibridge. ML with callcc is unsound. Message to the TYPES mailing list, July 1991. [ bib | .html ] |
| [306] | Robert Harper and Benjamin Pierce. A record calculus based on symmetric concatenation. In ACM Symposium on Principles of Programming Languages (POPL), pages 131-142, January 1991. [ bib | .ps ] |
| [307] | Michael A. Harrison, Walter L. Ruzzo, and Jeffrey D. Ullman. Protection in operating systems. Communications of the ACM, 19(8):461-471, August 1976. [ bib | http ] |
| [308] | Matthew S. Hecht and Jeffrey D. Ullman. Analysis of a simple algorithm for global data flow problems. In ACM Symposium on Principles of Programming Languages (POPL), pages 207-217, 1973. [ bib | http ] |
| [309] | Bastiaan Heeren and Jurriaan Hage. Parametric type inferencing for Helium. Technical Report UU-CS-2002-035, University of Utrecht, Institute of Information and Computing Science, August 2002. [ bib | .pdf ] |
| [310] | Bastiaan Heeren, Jurriaan Hage, and Doaitse Swierstra. Generalizing Hindley-Milner type inference algorithms. Technical Report UU-CS-2002-031, University of Utrecht, Institute of Information and Computing Science, July 2002. [ bib | .pdf ] |
| [311] | Bastiaan Heeren, Johan Jeuring, Doaitse Swierstra, and Pablo Azero Alcocer. Improving type-error messages in functional languages. Technical Report UU-CS-2002-009, University of Utrecht, Institute of Information and Computing Science, February 2002. [ bib | .pdf ] |
| [312] | Nevin Heintze. Set based analysis of ML programs. Technical Report CMU-CS-93-193, Carnegie Mellon University, School of Computer Science, July 1993. [ bib | .ps ] |
| [313] | Nevin Heintze and David McAllester. Linear-time subtransitive control flow analysis. In ACM Conference on Programming Language Design and Implementation (PLDI), pages 261-272, 1997. [ bib | .ps ] |
| [314] | Nevin Heintze and Jon G. Riecke. The SLam calculus: Programming with secrecy and integrity. In ACM Symposium on Principles of Programming Languages (POPL), pages 365-377, January 1998. [ bib | .ps ] |
| [315] | Nevin Heintze and Olivier Tardieu. Ultra-fast aliasing analysis using CLA: A million lines of C code in a second. In ACM Conference on Programming Language Design and Implementation (PLDI), pages 254-263, 2001. [ bib | .ps ] |
| [316] | Simon Helsen and Peter Thiemann. Syntactic type soundness for the region calculus. In International Workshop on Higher Order Operational Techniques in Semantics (HOOTS), volume 41(3) of Electronic Notes in Theoretical Computer Science, pages 1-19, 2000. [ bib | .pdf ] |
| [317] | Fergus Henderson. Strong modes can change the world! Technical Report 96/11, Department of Computer Science, University of Melbourne, November 1992. [ bib | .ps.gz ] |
| [318] | Dimitri Hendriks and Vincent van Oostrom. Adbmal. In International Conference on Automated Deduction (CADE), volume 2741 of Lecture Notes in Computer Science, pages 136-150. Springer Verlag, 2003. [ bib | .ps ] |
| [319] | Fritz Henglein. Polymorphic type inference and semi-unification. PhD thesis, Rutgers University, April 1989. [ bib | .ps.gz ] |
| [320] | Fritz Henglein. Efficient type inference for higher-order binding-time analysis. In Conference on Functional Programming Languages and Computer Architecture (FPCA), volume 523 of Lecture Notes in Computer Science, pages 448-472. Springer Verlag, 1991. [ bib | .dvi.gz ] |
| [321] | Fritz Henglein. Type inference with polymorphic recursion. ACM Transactions on Programming Languages and Systems, 15(2):253-289, April 1993. [ bib | http ] |
| [322] | Fritz Henglein. Breaking through the n3 barrier: Faster object type inference. In Workshop on Foundations of Object-Oriented Languages (FOOL), 1997. [ bib ] |
| [323] | Fritz Henglein. Breaking through the n3 barrier: Faster object type inference. Theory and Practice of Object Systems, 5(1):57-72, 1999. [ bib | .ps.gz ] |
| [324] | Fritz Henglein and Jakob Rehof. The complexity of subtype entailment for simple types. In IEEE Symposium on Logic in Computer Science (LICS), pages 352-361, June 1997. [ bib | .ps ] |
| [325] | Fritz Henglein and Jakob Rehof. Constraint automata and the complexity of recursive subtype entailment. In International Colloquium on Automata, Languages and Programming, July 1998. [ bib | .ps ] |
| [326] | Matthew Hennessy. The security picalculus and non-interference. Technical Report 2000:05, University of Sussex, November 2000. [ bib | .ps.Z ] |
| [327] | Matthew Hennessy and James Riely. Information flow vs. resource access in the asynchronous pi-calculus. In International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science. Springer Verlag, July 2000. [ bib | .ps.gz ] |
| [328] | Mark Hepburn and David Wright. Trust in the pi-calculus. In International ACM Conference on Principles and Practice of Declarative Programming (PPDP), September 2001. [ bib ] |
| [329] | Tomoyuki Higuchi and Atsushi Ohori. A static type system for JVM access control. In ACM International Conference on Functional Programming (ICFP), pages 227-237, August 2003. [ bib | http ] |
| [330] | J. Roger Hindley. The principal type-scheme of an object in combinatory logic. Transactions of the American Mathematical Society, 146:29-60, 1969. [ bib | http ] |
| [331] | Ralf Hinze. Fun with phantom types. In Jeremy Gibbons and Oege de Moor, editors, The Fun of Programming, pages 245-262. Palgrave Macmillan, March 2003. [ bib | .pdf ] |
| [332] | Ralf Hinze and Simon Peyton Jones. Derivable type classes. In Haskell workshop, 2000. [ bib | .ps.gz ] |
| [333] | Tom Hirschowitz and Xavier Leroy. Mixin modules in a call-by-value setting. ACM Transactions on Programming Languages and Systems, 2004. To appear. [ bib | .ps.gz ] |
| [334] | Tom Hirschowitz, Xavier Leroy, and J. B. Wells. Call-by-value mixin modules: Reduction semantics, side effects, types. In European Symposium on Programming (ESOP), volume 2986 of Lecture Notes in Computer Science, pages 64-78. Springer Verlag, April 2004. [ bib | .ps.gz ] |
| [335] | My Hoang and John C. Mitchell. Lower bounds on type inference with subtypes. In ACM Symposium on Principles of Programming Languages (POPL), pages 176-185, January 1995. [ bib | http ] |
| [336] | C. A. R. Hoare. Algorithm 65: find. Communications of the ACM, 4(7):321-322, July 1961. [ bib | http ] |
| [337] | C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576-580, 1969. [ bib | http ] |
| [338] | C. A. R. Hoare. Proof of a program: FIND. Communications of the ACM, 14(1):39-45, January 1971. [ bib | http ] |
| [339] | C. A. R. Hoare. Proof of correctness of data representations. Acta Informatica, 4:271-281, 1972. [ bib ] |
| [340] | Martin Hofmann and Benjamin Pierce. A unifying type-theoretic framework for objects. Journal of Functional Programming, 5(4):593-635, October 1995. Previous versions appeared in the Symposium on Theoretical Aspects of Computer Science, 1994, (pages 251-262) and, under the title “An Abstract View of Objects and Subtyping (Preliminary Report),” as University of Edinburgh, LFCS technical report ECS-LFCS-92-226, 1992. [ bib | .ps ] |
| [341] | Kohei Honda, Vasco Vasconcelos, and Nobuko Yoshida. Secure information flow as typed process behaviour. Technical Report QMW-DCS-1999-767, Queen Mary and Westfield College, University of London, December 1999. [ bib | .ps.gz ] |
| [342] | Kohei Honda, Vasco Vasconcelos, and Nobuko Yoshida. Secure information flow as typed process behaviour. In European Symposium on Programming (ESOP), volume 1782 of Lecture Notes in Computer Science, pages 180-199. Springer Verlag, March 2000. [ bib | .ps.gz ] |
| [343] | Kohei Honda and Nobuko Yoshida. A uniform type structure for secure information flow. In ACM Symposium on Principles of Programming Languages (POPL), pages 81-92, January 2002. [ bib | .ps.gz ] |
| [344] | Kohei Honda and Nobuko Yoshida. A compositional logic for polymorphic higher-order functions. In International ACM Conference on Principles and Practice of Declarative Programming (PPDP), pages 191-202, August 2004. [ bib | .pdf.gz ] |
| [345] | Furio Honsell, Marino Miculan, and Ivan Scagnetto. An axiomatic approach to metareasoning on nominal algebras in HOAS. In International Colloquium on Automata, Languages and Programming, volume 2076 of Lecture Notes in Computer Science, pages 963-978. Springer Verlag, 2001. [ bib | .pdf ] |
| [346] | John E. Hopcroft. An nlogn algorithm for minimizing states in a finite automaton. In Z. Kohavi, editor, Theory of Machines and Computations, pages 189-196. Academic Press, 1971. [ bib ] |
| [347] | John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman. Introduction to automata theory, languages, and computation. Addison-Wesley, 2000. [ bib | .html ] |
| [348] | R. Nigel Horspool and Michael Whitney. Even faster LR parsing. Software - Practice & Experience, 20(6):515-535, June 1990. [ bib | .pdf ] |
| [349] | Susan Horwitz, Thomas Reps, and Mooly Sagiv. Demand interprocedural dataflow analysis. In ACM Symposium on the Foundations of Software Engineering (FSE), October 1995. [ bib | .ps ] |
| [350] | Haruo Hosoya and Benjamin C. Pierce. Regular expression pattern matching for XML. Journal of Functional Programming, 13(6):961-1004, November 2003. [ bib | http ] |
| [351] | Thierry Hubert and Claude Marché. Separation analysis for deductive verification. In Heap Analysis and Verification (HAV), March 2007. [ bib | .pdf ] |
| [352] | Paul Hudak, John Hughes, Simon Peyton Jones, and Philip Wadler. A history of Haskell: being lazy with class. In ACM SIGPLAN Conference on History of Programming Languages, June 2007. [ bib | .pdf ] |
| [353] | Gérard Huet. Résolution d'équations dans des langages d'ordre 1, 2, ..., ω. PhD thesis, Université Paris 7, September 1976. [ bib ] |
| [354] | John Hughes. Why functional programming matters. Computer Journal, 32(2):98-107, 1989. [ bib | .pdf ] |
| [355] | Atsushi Igarashi and Naoki Kobayashi. Type reconstruction for linear π-calculus with I/O subtyping. Information and Computation, 161:1-44, August 2000. [ bib | .ps.gz ] |
| [356] | Daniel Jackson and Mandana Vaziri. Finding bugs with a constraint solver. In International Symposium on Software Testing and Analysis (ISSTA), August 2000. [ bib | .pdf ] |
| [357] | Suresh Jagannathan and Andrew Wright. Effective flow analysis for avoiding run-time checks. In Static Analysis Symposium (SAS), volume 983 of Lecture Notes in Computer Science. Springer Verlag, September 1995. [ bib | .ps.gz ] |
| [358] | C. Barry Jay. The pattern calculus. ACM Transactions on Programming Languages and Systems, 26(6):911-937, November 2004. [ bib | .pdf ] |
| [359] | Thomas Jensen. Inference of polymorphic and conditional strictness properties. In ACM Symposium on Principles of Programming Languages (POPL), pages 209-221. ACM Press, January 1998. [ bib | .ps ] |
| [360] | Thomas Jensen, Daniel Le Métayer, and Tommy Thorn. Verifying security properties of control-flow graphs. In IEEE Symposium on Security and Privacy (S&P), pages 89-105, May 1999. [ bib | .ps ] |
| [361] | Somesh Jha, Jens Palsberg, and Tian Zhao. Efficient type matching. In International Conference on Foundations of Software Science and Computation Structures (FOSSACS), volume 2303 of Lecture Notes in Computer Science, pages 187-204. Springer Verlag, April 2002. [ bib | .pdf ] |
| [362] | Limin Jia, Frances Spalding, David Walker, and Neal Glew. Certifying compilation for a language with stack allocation. In IEEE Symposium on Logic in Computer Science (LICS), pages 407-416, June 2005. [ bib | .pdf ] |
| [363] | Trevor Jim. What are principal typings and what are they good for? Technical Report MIT/LCS TM-532, Massachusetts Institute of Technology, August 1995. [ bib | .ps.gz ] |
| [364] | Trevor Jim. A polar type system. In Workshop on Intersection Types and Related Systems (ITRS), volume 8 of Proceedings in Informatics. Carleton Scientific, 2000. [ bib | .ps.gz ] |
| [365] | Trevor Jim and Jens Palsberg. Type inference in systems of recursive types with subtyping. Manuscript, 1999. [ bib | .pdf ] |
| [366] | Gregory F. Johnson and Janet A. Walz. A maximum-flow approach to anomaly isolation in unification-based incremental type inference. In ACM Symposium on Principles of Programming Languages (POPL), pages 44-57, January 1986. [ bib ] |
| [367] | Stephen C. Johnson. Yacc: Yet another compiler-compiler. Computing Science Technical Report 32, Bell Laboratories, 1975. [ bib | .ps ] |
| [368] | Steven C. Johnson. Yacc: Yet another compiler compiler. In UNIX Programmer's Manual, volume 2, pages 353-387. Holt, Rinehart, and Winston, 1979. [ bib | http ] |
| [369] | Thomas Johnsson. Lambda lifting: Transforming programs to recursive equations. In Jean-Pierre Jouannaud, editor, Conference on Functional Programming Languages and Computer Architecture (FPCA), volume 201 of Lecture Notes in Computer Science, pages 190-203. Springer Verlag, 1985. [ bib | http ] |
| [370] | Mark P. Jones. A theory of qualified types. In European Symposium on Programming (ESOP), volume 582 of Lecture Notes in Computer Science. Springer Verlag, February 1992. [ bib | .html ] |
| [371] | Mark P. Jones. Dictionary-free overloading by partial evaluation. In ACM Workshop on Evaluation and Semantics-Based Program Manipulation (PEPM), June 1994. [ bib | .ps ] |
| [372] | Mark P. Jones. Qualified types: Theory and practice. Cambridge University Press, November 1994. [ bib ] |
| [373] | Mark P. Jones. Simplifying and improving qualified types. Technical Report YALEU/DCS/RR-1040, Yale University, June 1994. [ bib | .ps.Z ] |
| [374] | Mark P. Jones. From Hindley-Milner types to first-class structures. Research Report YALEU/DCS/RR-1075, Yale University, June 1995. [ bib | .html ] |
| [375] | Mark P. Jones. Using parameterized signatures to express modular structure. In ACM Symposium on Principles of Programming Languages (POPL), January 1996. [ bib | .html ] |
| [376] | Mark P. Jones. Typing Haskell in Haskell. In Haskell workshop, October 1999. [ bib | http ] |
| [377] | Mark P. Jones and Simon Peyton Jones. Lightweight extensible records for Haskell. In Haskell workshop, October 1999. [ bib | .ps.gz ] |
| [378] | Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. Simple unification-based type inference for GADTs. Submitted, November 2005. [ bib | .pdf ] |
| [379] | Jean-Pierre Jouannaud and Claude Kirchner. Solving equations in abstract algebras: a rule-based survey of unification. Technical Report 561, Université Paris-Sud, April 1990. [ bib ] |
| [380] | Jean-Pierre Jouannaud and Claude Kirchner. Solving equations in abstract algebras: a rule-based survey of unification. In Jean-Louis Lassez and Gordon Plotkin, editors, Computational Logic. Essays in honor of Alan Robinson, chapter 8, pages 257-321. MIT Press, 1991. [ bib ] |
| [381] | John B. Kam and Jeffrey D. Ullman. Global data flow analysis and iterative algorithms. Journal of the ACM, 23(1):158-171, January 1976. [ bib | http ] |
| [382] | John B. Kam and Jeffrey D. Ullman. Monotone data flow analysis frameworks. Acta Informatica, 7:305-317, 1977. [ bib ] |
| [383] | Haim Kaplan and Robert E. Tarjan. Purely functional, real-time deques with catenation. Journal of the ACM, 46(5):577-603, 1999. [ bib | .ps ] |
| [384] | Deepak Kapur and Hantao Zhang. An overview of Rewrite Rule Laboratory (RRL). J. Comput. Appl. Math., 29(2):91-114, 1995. [ bib | .ps.gz ] |
| [385] | Torbjörn Keisu. Finite and rational tree constraints. Bulletin of the IGPL, 2(2):167-204, 1994. [ bib | .ps.gz ] |
| [386] | Torbjörn Keisu. Tree constraints. PhD thesis, The Royal Institute of Technology (KTH), May 1994. [ bib | .ps.gz ] |
| [387] | Andrew Kennedy. Dimension types. In European Symposium on Programming (ESOP), volume 788 of Lecture Notes in Computer Science. Springer Verlag, 1994. [ bib | .pdf ] |
| [388] | Andrew Kennedy. Type inference and equational theories. Technical Report LIX/RR/96/09, École Polytechnique, September 1996. [ bib ] |
| [389] | Manfred Kerber. How to prove higher order theorems in first order logic. In International Joint Conferences on Artificial Intelligence, pages 137-142, 1991. [ bib | .pdf ] |
| [390] | A. J. Kfoury, J. Tiuryn, and P. Urzyczyn. Type reconstruction in the presence of polymorphic recursion. ACM Transactions on Programming Languages and Systems, 15(2):290-311, 1993. [ bib | http ] |
| [391] | Assaf J. Kfoury, Jerzy Tiuryn, and Pawel Urzyczyn. ML typability is DEXPTIME-complete. In Colloquium on Trees in Algebra and Programming, volume 431 of Lecture Notes in Computer Science, pages 206-220. Springer Verlag, May 1990. [ bib | http ] |
| [392] | Assaf J. Kfoury and J. B. Wells. Principality and type inference for intersection types using expansion variables. Theoretical Computer Science, 311(1-3):1-70, 2004. [ bib | .html ] |
| [393] | Richard B. Kieburtz. Taming effects with monadic typing. In ACM International Conference on Functional Programming (ICFP), pages 51-62, 1998. [ bib | http ] |
| [394] | Richard B. Kieburtz. P-logic: Property verification for Haskell programs. Draft, August 2002. [ bib | .pdf ] |
| [395] | Gary A. Kildall. A unified approach to global program optimization. In ACM Symposium on Principles of Programming Languages (POPL), pages 194-206, October 1973. [ bib | http ] |
| [396] | Ik-Soon Kim, Kwangkeun Yi, and Cristiano Calcagno. A polymorphic modal type system for Lisp-like multi-staged languages. In ACM Symposium on Principles of Programming Languages (POPL), pages 257-268, 2006. [ bib | .pdf ] |
| [397] | David King and Philip Wadler. Combining monads. In Workshop on Functional Programming. Springer Verlag, 1992. [ bib | .ps.gz ] |
| [398] | Kevin Knight. Unification: a multidisciplinary survey. ACM Computing Surveys, 21(1):93-124, March 1989. [ bib | http ] |
| [399] | Donald E. Knuth. On the translation of languages from left to right. Information & Control, 8(6):607-639, December 1965. [ bib ] |
| [400] | Donald E. Knuth. A generalization of Dijkstra's algorithm. Information Processing Letters, 6(1):1-5, February 1977. [ bib ] |
| [401] | Naoki Kobayashi. A partially deadlock-free typed process calculus. ACM Transactions on Programming Languages and Systems, 20(2):436-482, March 1998. [ bib | http ] |
| [402] | Naoki Kobayashi. Type-based useless variable elimination. In ACM Workshop on Evaluation and Semantics-Based Program Manipulation (PEPM), pages 84-93, January 2000. [ bib | .ps.gz ] |
| [403] | Naoki Kobayashi, Benjamin C. Pierce, and David N. Turner. Linearity and the Pi-Calculus. ACM Transactions on Programming Languages and Systems, 21(5):914-947, September 1999. [ bib | http ] |
| [404] | Naoki Kobayashi, Shin Saito, and Eijiro Sumii. An implicitly-typed deadlock-free process calculus. In International Conference on Concurrency Theory (CONCUR), volume 1877 of Lecture Notes in Computer Science, pages 489-503. Springer Verlag, August 2000. [ bib | .ps.gz ] |
| [405] | Yasunori Koda and Frank Ruskey. A Gray code for the ideals of a forest poset. Journal of Algorithms, 15(2):324-340, September 1993. [ bib | .ps ] |
| [406] | Eugene Kohlbecker, Daniel P. Friedman, Matthias Felleisen, and Bruce Duba. Hygienic macro expansion. In ACM Symposium on Lisp and Functional Programming (LFP), pages 151-161, 1986. [ bib | http ] |
| [407] | Eugene E. Kohlbecker and Mitchell Wand. Macro-by-example: Deriving syntactic transformations from their specifications. In ACM Symposium on Principles of Programming Languages (POPL), pages 77-84, January 1987. [ bib | http ] |
| [408] | Larry Koved, Marco Pistoia, and Aaron Kershenbaum. Access rights analysis for Java. In ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 359-372, November 2002. [ bib | .pdf ] |
| [409] | Dexter Kozen, Jens Palsberg, and Michael I. Schwartzbach. Efficient recursive subtyping. Mathematical Structures in Computer Science, 5(1):113-125, 1995. [ bib | .pdf ] |
| [410] | Shriram Krishnamurthi, Matthias Felleisen, and Bruce F. Duba. From macros to reusable generative programming. In Generative and Component-Based Software Engineering, volume 1799 of Lecture Notes in Computer Science, pages 105-120. Springer Verlag, September 1999. [ bib | .ps ] |
| [411] | Viktor Kuncak and Martin Rinard. On the theory of structural subtyping. Technical Report 879, MIT Laboratory for Computer Science, January 2003. [ bib | .ps ] |
| [412] | Viktor Kuncak and Martin Rinard. Structural subtyping of non-recursive types is decidable. In IEEE Symposium on Logic in Computer Science (LICS), June 2003. [ bib | .pdf ] |
| [413] | Charlie Lai, Li Gong, Larry Koved, Anthony J. Nadalin, and Roland Schemers. User authentication and authorization in the Java platform. In Annual Computer Security Applications Conference, pages 285-290, December 1999. [ bib | .pdf ] |
| [414] | Butler W. Lampson. A note on the confinement problem. Communications of the ACM, 16(10):613-615, October 1973. [ bib | .html ] |
| [415] | Peter J. Landin. The mechanical evaluation of expressions. Computer Journal, 6(4):308-320, January 1964. [ bib ] |
| [416] | Peter J. Landin. Correspondence between ALGOL 60 and Church's lambda-notation: part I. Communications of the ACM, 8(2):89-101, 1965. [ bib | http ] |
| [417] | J.-L. Lassez, V. L. Nguyen, and E. A. Sonenberg. Fixed point theorems and semantics: a folk tale. Information Processing Letters, 14(3):112-116, May 1982. [ bib | http ] |
| [418] | Jean-Louis Lassez, Michael J. Maher, and Kim G. Marriott. Unification revisited. In Jack Minker, editor, Foundations of Deductive Databases and Logic Programming, chapter 15, pages 587-625. Morgan Kaufmann, 1988. [ bib ] |
| [419] | Konstantin Läufer and Martin Odersky. Polymorphic type inference and abstract data types. ACM Transactions on Programming Languages and Systems, 16(5):1411-1430, September 1994. [ bib | .pdf ] |
| [420] | Didier Le Botlan and Didier Rémy. MLF: Raising ML to the power of system F. In ACM International Conference on Functional Programming (ICFP), pages 27-38, August 2003. [ bib | .pdf ] |
| [421] | Fabrice Le Fessant and Luc Maranget. Optimizing pattern matching. In ACM International Conference on Functional Programming (ICFP), 2001. [ bib | .ps.gz ] |
| [422] | Christopher League, Zhong Shao, and Valery Trifonov. Representing Java classes in a typed intermediate language. In ACM International Conference on Functional Programming (ICFP), pages 183-196, September 1999. [ bib | .html ] |
| [423] | Christopher League, Zhong Shao, and Valery Trifonov. Type-preserving compilation of Featherweight Java. ACM Transactions on Programming Languages and Systems, 24(2):112-152, March 2002. [ bib | .html ] |
| [424] | Christopher League, Zhong Shao, and Valery Trifonov. Precision in practice: a type-preserving Java compiler. In International Conference on Compiler Construction (CC), volume 2622 of Lecture Notes in Computer Science, pages 106-120. Springer Verlag, April 2003. [ bib | .html ] |
| [425] | Oukseh Lee and Kwangkeun Yi. Proofs about a folklore let-polymorphic type inference algorithm. ACM Transactions on Programming Languages and Systems, 20(4):707-723, 1998. [ bib | http ] |
| [426] | K. Rustan M. Leino and Greg Nelson. Data abstraction and information hiding. ACM Transactions on Programming Languages and Systems, 24(5):491-553, 2002. [ bib | .pdf ] |
| [427] | Xavier Leroy. Polymorphic typing of an algorithmic language. Research Report 1778, INRIA, October 1992. [ bib | .ps.gz ] |
| [428] | Xavier Leroy. Typage polymorphe d'un langage algorithmique. PhD thesis, Université Paris 7, June 1992. [ bib | .ps.gz ] |
| [429] | Xavier Leroy. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In ACM Symposium on Principles of Programming Languages (POPL), pages 42-54, January 2006. [ bib | .pdf ] |
| [430] | Xavier Leroy, Damien Doligez, Jacques Garrigue, Didier Rémy, and Jérôme Vouillon. The Objective Caml system, October 2005. [ bib | http ] |
| [431] | Xavier Leroy, Damien Doligez, Michel Mauny, and Pierre Weis. The Caml Light system, release 0.75, 2002. [ bib | http ] |
| [432] | Xavier Leroy and François Pottier. Notes du cours de DEA « typage et programmation », December 2002. [ bib | .ps.gz ] |
| [433] | Stéphane Lescuyer. Codage de la logique du premier ordre polymorphe multi-sortée dans la logique sans sortes. Master's thesis, Master Parisien de Recherche en Informatique, 2006. [ bib | .pdf ] |
| [434] | Pierre Letouzey. Programmation fonctionnelle certifiée - l'extraction de programmes dans l'assistant Coq. PhD thesis, Université Paris 11, July 2004. [ bib | .ps.gz ] |
| [435] | Jeffrey Lewis, Mark Shields, Erik Meijer, and John Launchbury. Implicit parameters: Dynamic scoping with static types. In ACM Symposium on Principles of Programming Languages (POPL), pages 108-118, January 2000. [ bib | .ps ] |
| [436] | John Longley. When is a functional program not a functional program? In ACM International Conference on Functional Programming (ICFP), pages 1-7, September 1999. [ bib | http ] |
| [437] | John Longley and Randy Pollack. Reasoning about CBV functional programs in Isabelle/HOL. In International Conference on Theorem Proving in Higher Order Logics (TPHOLs), volume 3223 of Lecture Notes in Computer Science, pages 201-216. Springer Verlag, September 2004. [ bib | .pdf ] |
| [438] | Ralf Lämmel and Simon Peyton Jones. Scrap your boilerplate with class: extensible generic functions. Submitted, April 2005. [ bib | .ps ] |
| [439] | Ralf Lämmel, Joost Visser, and Jan Kort. Dealing with large bananas. In Workshop on Generic Programming, pages 46-59, July 2000. [ bib | .ps ] |
| [440] | David B. MacQueen, Gordon D. Plotkin, and Ravi Sethi. An ideal model for recursive polymorphic types. Information and Control, 71(1-2):95-130, October-November 1986. [ bib ] |
| [441] | Michael J. Maher. Complete axiomatizations of the algebras of finite, rational and infinite trees. In IEEE Symposium on Logic in Computer Science (LICS), pages 348-357, July 1988. [ bib ] |
| [442] | Harry G. Mairson, Paris C. Kanellakis, and John C. Mitchell. Unification and ML type reconstruction. In J.-L. Lassez and G. Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson, pages 444-478. MIT Press, 1991. [ bib ] |
| [443] | Claude Marché, Christine Paulin-Mohring, and Xavier Urbain. The Krakatoa tool for certification of Java/JavaCard programs annotated in JML. Journal of Logic and Algebraic Programming, 58(1-2):89-106, 2004. [ bib | .ps.gz ] |
| [444] | Simon Marlow and Andy Gill. Happy: the parser generator for Haskell, April 2004. [ bib | http ] |
| [445] | Simon Marlow and Philip Wadler. A practical subtyping system for Erlang. In ACM International Conference on Functional Programming (ICFP), pages 136-149, June 1997. [ bib ] |
| [446] | Kim Marriott and Martin Odersky. Negative Boolean constraints. Technical Report 94/203, Monash University, August 1994. [ bib | .ps.gz ] |
| [447] | Alberto Martelli and Ugo Montanari. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems, 4(2):258-282, April 1982. [ bib | http ] |
| [448] | Michel Mauny and François Pottier. An implementation of Caml Light with existential types. Technical Report 2183, INRIA, 1993. [ bib | .ps.gz ] |
| [449] | Bruce J. McAdam. On the Unification of Substitutions in Type Inference. In Implementation of Functional Languages (IFL), volume 1595 of Lecture Notes in Computer Science, pages 139-154. Springer Verlag, September 1998. [ bib | .ps ] |
| [450] | David McAllester. On the complexity analysis of static analyses. Journal of the ACM, 49(4):512-537, July 2002. [ bib | http ] |
| [451] | David McAllester. A logical algorithm for ML type inference. In Rewriting Techniques and Applications (RTA), volume 2706 of Lecture Notes in Computer Science, pages 436-451. Springer Verlag, June 2003. [ bib | .ps ] |
| [452] | Conor McBride and James McKinna. I am not a number: I am a free variable. In Haskell workshop, September 2004. [ bib | .ps.gz ] |
| [453] | James McKinna and Randy Pollack. Pure type systems formalized. In International Conference on Typed Lambda Calculi and Applications (TLCA), number 664 in Lecture Notes in Computer Science, pages 289-305. Springer Verlag, March 1993. [ bib | .ps.gz ] |
| [454] | James McKinna and Randy Pollack. Some lambda calculus and type theory formalized. Journal of Automated Reasoning, 23(3-4):373-409, 1999. [ bib ] |
| [455] | John McLean. A general theory of composition for trace sets closed under selective interleaving functions. In IEEE Symposium on Security and Privacy (S&P), 1994. [ bib | .ps ] |
| [456] | John McLean. Security models. In John Marciniak, editor, Encyclopedia of Software Engineering. John Wiley & Sons, 1994. [ bib | .ps ] |
| [457] | Catherine Meadows. Formal verification of cryptographic protocols: A survey. In Advances in Cryptology - ASIACRYPT'94, volume 917 of Lecture Notes in Computer Science, pages 133-150. Springer Verlag, 1995. [ bib | .ps ] |
| [458] | Farhad Mehta and Tobias Nipkow. Proving pointer programs in higher-order logic. Information and Computation, 199(1-2):200-227, 2005. [ bib | .ps.gz ] |
| [459] | David Melski and Thomas Reps. Interconvertibility of a class of set constraints and context-free language reachability. Theoretical Computer Science, 248(1-2), November 2000. [ bib | .ps ] |
| [460] | Dale Miller. An extension to ML to handle bound variables in data structures. In Logical Frameworks BRA Workshop, May 1990. [ bib | .pdf ] |
| [461] | Todd Millstein and Craig Chambers. Modular statically typed multimethods. In European Conference on Object-Oriented Programming, volume 1628 of Lecture Notes in Computer Science, pages 279-303. Springer Verlag, June 1999. [ bib | .ps ] |
| [462] | Todd Millstein and Craig Chambers. Modular statically typed multimethods. Information and Computation, 175(1):76-118, May 2002. [ bib | .ps ] |
| [463] | Robin Milner. Implementation and applications of Scott's logic for computable functions. In Proceedings of the ACM conference on proving assertions about programs, pages 1-6, January 1972. [ bib | http ] |
| [464] | Robin Milner. Logic for computable functions - description of a machine implementation. Technical Report CS-TR-72-288, Stanford University, Department of Computer Science, May 1972. [ bib | .pdf ] |
| [465] | Robin Milner. Models of LCF. Technical Report CS-TR-73-332, Stanford University, Department of Computer Science, January 1973. [ bib | .pdf ] |
| [466] | Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17(3):348-375, December 1978. [ bib | .pdf ] |
| [467] | Robin Milner. The polyadic π-calculus: a tutorial. Technical Report ECS-LFCS-91-180, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, October 1991. [ bib | .ps.Z ] |
| [468] | Robin Milner and Davide Sangiorgi. Barbed bisimulation. In International Colloquium on Automata, Languages and Programming, volume 623 of Lecture Notes in Computer Science, pages 685-695. Springer Verlag, July 1992. [ bib | .ps.gz ] |
| [469] | Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The definition of Standard ML - revised. MIT Press, May 1997. [ bib ] |
| [470] | Yasuhiko Minamide. A functional representation of data structures with a hole. In ACM Symposium on Principles of Programming Languages (POPL), pages 75-84, January 1998. [ bib | .pdf ] |
| [471] | Yasuhiko Minamide, Greg Morrisett, and Robert Harper. Typed closure conversion. In ACM Symposium on Principles of Programming Languages (POPL), pages 271-283, January 1996. [ bib | .ps ] |
| [472] | David G. Mitchell. A SAT solver primer. Bulletin of the EATCS, 85:112-133, February 2005. [ bib | .pdf ] |
| [473] | John C. Mitchell. Coercion and type inference. In ACM Symposium on Principles of Programming Languages (POPL), pages 175-185, January 1984. [ bib | http ] |
| [474] | John C. Mitchell. Polymorphic type inference and containment. Information and Computation, 76(2-3):211-249, 1988. [ bib | http ] |
| [475] | John C. Mitchell. Type inference with simple subtypes. Journal of Functional Programming, 1(3):245-286, July 1991. [ bib ] |
| [476] | John C. Mitchell. Foundations for programming languages. MIT Press, 1996. [ bib ] |
| [477] | Masaaki Mizuno and David A. Schmidt. A security flow control algorithm and its denotational semantics correctness proof. Formal Aspects of Computing, 4(6A):727-754, 1992. [ bib | .ps.Z ] |
| [478] | Eugenio Moggi. An abstract view of programming languages. Technical Report ECS-LFCS-90-113, University of Edinburgh, June 1989. [ bib | .ps.gz ] |
| [479] | Eugenio Moggi. Computational λ-calculus and monads. In IEEE Symposium on Logic in Computer Science (LICS), pages 14-23, June 1989. [ bib | .ps.gz ] |
| [480] | Eugenio Moggi. Notions of computation and monads. Information and Computation, 93(1), 1991. [ bib | .pdf ] |
| [481] | Anders Møller and Michael I. Schwartzbach. The pointer assertion logic engine. In ACM Conference on Programming Language Design and Implementation (PLDI), pages 221-231, June 2001. [ bib | .pdf ] |
| [482] | Stefan Monnier. Statically tracking state with typed regions. Draft, August 2007. [ bib | .pdf ] |
| [483] | James H. Morris, Donald E. Knuth, and Vaughan R. Pratt. Fast pattern matching in strings. SIAM Journal on Computing, 6(2):323-350, June 1977. [ bib | .pdf ] |
| [484] | Greg Morrisett and Robert Harper. Typed closure conversion for recursively-defined functions (extended abstract). In International Workshop on Higher Order Operational Techniques in Semantics (HOOTS), volume 10 of Electronic Notes in Theoretical Computer Science. Elsevier Science, 1998. [ bib | .ps ] |
| [485] | Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From system F to typed assembly language. ACM Transactions on Programming Languages and Systems, 21(3):528-569, May 1999. [ bib | .pdf ] |
| [486] | Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In Design Automation Conference (DAC), July 2001. [ bib | .pdf ] |
| [487] | Martin Müller. A constraint-based recast of ML-polymorphism. In International Workshop on Unification, June 1994. Technical Report 94-R-243, CRIN, Nancy, France. [ bib | .ps ] |
| [488] | Martin Müller. Notes on HM(X). August 1998. [ bib | .ps.gz ] |
| [489] | Martin Müller, Joachim Niehren, and Ralf Treinen. The first-order theory of ordering constraints over feature trees. Discrete Mathematics and Theoretical Computer Science, 4(2):193-234, 2001. [ bib | .ps ] |
| [490] | Martin Müller and Susumu Nishimura. Type inference for first-class messages with feature constraints. In Asian Computer Science Conference (ASIAN), volume 1538 of Lecture Notes in Computer Science, pages 169-187. Springer Verlag, December 1998. [ bib | .ps ] |
| [491] | Martin Müller and Susumu Nishimura. Type inference for first-class messages with feature constraints. International Journal of Foundations of Computer Science, 11(1):29-63, 2000. [ bib ] |
| [492] | Alan Mycroft. Polymorphic type schemes and recursive definitions. In International Symposium on Programming, volume 167 of Lecture Notes in Computer Science, pages 217-228. Springer Verlag, April 1984. [ bib | http ] |
| [493] | Andrew C. Myers. JFlow: practical mostly-static information flow control. In ACM Symposium on Principles of Programming Languages (POPL), pages 228-241, January 1999. [ bib | .ps.gz ] |
| [494] | Andrew C. Myers. Mostly-static decentralized information flow control. PhD thesis, Massachusetts Institute of Technology, January 1999. Technical Report MIT/LCS/TR-783. [ bib | .ps.gz ] |
| [495] | Andrew C. Myers and Barbara Liskov. A decentralized model for information flow control. ACM Operating Systems Review, 31(5):129-142, October 1997. [ bib | .html ] |
| [496] | Andrew C. Myers and Barbara Liskov. Complete, safe information flow with decentralized labels. In IEEE Symposium on Security and Privacy (S&P), pages 186-197, May 1998. [ bib | .html ] |
| [497] | Andrew C. Myers and Barbara Liskov. Protecting privacy using the decentralized label model. ACM Transactions on Software Engineering and Methodology, 9(4):410-442, October 2000. [ bib | .ps.gz ] |
| [498] | Andrew C. Myers and Andrei Sabelfeld. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21(1):5-19, January 2003. [ bib | .pdf ] |
| [499] | Martin Müller, Joachim Niehren, and Andreas Podelski. Ordering constraints over feature trees. Constraints, an International Journal, 5(1-2):7-42, 2000. [ bib | .ps.gz ] |
| [500] | Olaf Müller, Tobias Nipkow, David von Oheimb, and Oskar Slotosch. HOLCF = HOL + LCF. Journal of Functional Programming, 9:191-223, 1999. [ bib | .ps.gz ] |
| [501] | Gopalan Nadathur and Xiaochu Qi. Explicit substitutions in the reduction of lambda terms. In International ACM Conference on Principles and Practice of Declarative Programming (PPDP), pages 195-206, August 2003. [ bib | .ps ] |
| [502] | Aleksandar Nanevski. Meta-programming with names and necessity. Technical Report CMU-CS-02-123R, School of Computer Science, Carnegie Mellon University, November 2002. [ bib | .ps ] |
| [503] | Aleksandar Nanevski, Amal Ahmed, Greg Morrisett, and Lars Birkedal. Abstract predicates and mutable ADTs in Hoare type theory. In European Symposium on Programming (ESOP), Lecture Notes in Computer Science. Springer Verlag, March 2007. [ bib | .pdf ] |
| [504] | Aleksandar Nanevski, Greg Morrisett, and Lars Birkedal. Polymorphism and separation in Hoare type theory. In ACM International Conference on Functional Programming (ICFP), pages 62-73, September 2006. [ bib | .pdf ] |
| [505] | Wolfgang Naraschewski and Tobias Nipkow. Type inference verified: Algorithm W in Isabelle/HOL. Journal of Automated Reasoning, 23:299-318, 1999. [ bib | .ps.gz ] |
| [506] | David A. Naumann. On assertion-based encapsulation for object invariants and simulations. Formal Aspects of Computing, 19(2):205-224, 2007. [ bib | .pdf ] |
| [507] | Jan Nicklisch and Simon Peyton Jones. An exploration of modular programs. In Functional Programming Workshop, July 1996. [ bib | .ps.gz ] |
| [508] | Joachim Niehren, Martin Müller, and Andreas Podelski. Inclusion constraints over non-empty sets of trees. In International Joint Conference on Theory and Practice of Software Development (TAPSOFT), volume 1214 of Lecture Notes in Computer Science, pages 217-231. Springer Verlag, April 1997. [ bib | .ps ] |
| [509] | Joachim Niehren and Tim Priesnitz. Non-structural subtype entailment in automata theory. In International Symposium on Theoretical Aspects of Computer Software (TACS). Springer Verlag, October 2001. [ bib | .ps.gz ] |
| [510] | Joachim Niehren and Tim Priesnitz. Non-structural subtype entailment in automata theory. Information and Computation, 186(2):319-354, 2003. [ bib | .pdf ] |
| [511] | Lasse R. Nielsen. A denotational investigation of defunctionalization. Technical Report RS-00-47, BRICS, December 2000. [ bib | http ] |
| [512] | Flemming Nielson, Hanne Riis Nielson, and Helmut Seidl. A succinct solver for ALFP. Nordic Journal of Computing, 9(4):335-372, 2002. [ bib | .pdf ] |
| [513] | Susumu Nishimura. Static typing for dynamic messages. In ACM Symposium on Principles of Programming Languages (POPL), pages 266-278, January 1998. [ bib | .ps.gz ] |
| [514] | Martin Odersky. Observers for linear types. In European Symposium on Programming (ESOP), volume 582 of Lecture Notes in Computer Science, pages 390-407. Springer Verlag, 1992. [ bib | .ps.gz ] |
| [515] | Martin Odersky. A functional theory of local names. In ACM Symposium on Principles of Programming Languages (POPL), pages 48-59, January 1994. [ bib | .ps.gz ] |
| [516] | Martin Odersky and Konstantin Läufer. An extension of ML with first-class abstract types. In ACM Workshop on ML and its Applications, pages 78-91, June 1992. [ bib | .pdf ] |
| [517] | Martin Odersky and Konstantin Läufer. Putting type annotations to work. In ACM Symposium on Principles of Programming Languages (POPL), pages 54-67, January 1996. [ bib | .ps.gz ] |
| [518] | Martin Odersky, Martin Sulzmann, and Martin Wehr. Type inference with constrained types. Theory and Practice of Object Systems, 5(1):35-55, 1999. [ bib | .ps ] |
| [519] | Martin Odersky, Philip Wadler, and Martin Wehr. A second look at overloading. In Conference on Functional Programming Languages and Computer Architecture (FPCA), pages 135-146, June 1995. [ bib | .ps.gz ] |
| [520] | Martin Odersky, Christoph Zenger, Matthias Zenger, and Gang Chen. A functional view of join. Technical Report ACRC-99-016, University of South Australia, 1999. [ bib | .ps.gz ] |
| [521] | Martin Odersky and Matthias Zenger. Scalable component abstractions. In ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 41-57, October 2005. [ bib | .pdf ] |
| [522] | Martin Odersky, Matthias Zenger, and Christoph Zenger. Colored local type inference. In ACM Symposium on Principles of Programming Languages (POPL), pages 41-53, 2001. [ bib | .ps.gz ] |
| [523] | Peter O'Hearn. On bunched typing. Journal of Functional Programming, 13(4):747-796, 2003. [ bib | .pdf ] |
| [524] | Peter O'Hearn, Hongseok Yang, and John C. Reynolds. Separation and information hiding. In ACM Symposium on Principles of Programming Languages (POPL), pages 268-280, January 2004. [ bib | .pdf ] |
| [525] | Peter W. O'Hearn. Resources, concurrency and local reasoning. Theoretical Computer Science, 375(1-3):271-307, May 2007. [ bib | .pdf ] |
| [526] | Atsushi Ohori. A polymorphic record calculus and its compilation. ACM Transactions on Programming Languages and Systems, 17(6):844-895, November 1995. [ bib | http ] |
| [527] | Atsushi Ohori and Peter Buneman. Type inference in a database programming language. In ACM Symposium on Lisp and Functional Programming (LFP), pages 174-183, 1988. [ bib | .pdf ] |
| [528] | Chris Okasaki. Purely functional data structures. Technical Report CMU-CS-96-177, School of Computer Science, Carnegie Mellon University, September 1996. [ bib | .pdf ] |
| [529] | Chris Okasaki. The role of lazy evaluation in amortized data structures. In ACM International Conference on Functional Programming (ICFP), pages 62-72, May 1996. [ bib | .ps ] |
| [530] | Chris Okasaki. Views for Standard ML. In ACM Workshop on ML, pages 14-23, September 1998. [ bib | .ps ] |
| [531] | Chris Okasaki. Purely functional data structures. Cambridge University Press, 1999. [ bib | http ] |
| [532] | Chris Okasaki and Andy Gill. Fast mergeable integer maps. In ACM Workshop on ML, pages 77-86, September 1998. [ bib | .ps ] |
| [533] | Ernst-Rüdiger Olderog. A characterization of Hoare's logic for programs with Pascal-like procedures. In ACM Symposium on Theory of Computing, pages 320-329, 1983. [ bib | http ] |
| [534] | Peter Ørbæk and Jens Palsberg. Trust in the λ-calculus. Journal of Functional Programming, 7(6):557-591, November 1997. [ bib | .pdf ] |
| [535] | Joseph O'Rourke. Computational geometry in C, second edition. Cambridge University Press, 1998. [ bib | .html ] |
| [536] | James William O'Toole, Jr. and David K. Gifford. Type reconstruction with first-class polymorphic values. In ACM Conference on Programming Language Design and Implementation (PLDI), pages 207-217, 1989. [ bib | .ps ] |
| [537] | David Pager. A practical general method for constructing LR(k) parsers. Acta Informatica, 7:249-268, 1977. [ bib ] |
| [538] | Robert Paige and Robert E. Tarjan. Three partition refinement algorithms. SIAM Journal on Computing, 16(6):973-989, December 1987. [ bib | .pdf ] |
| [539] | Jens Palsberg. Efficient inference of object types. Information and Computation, 123(2):198-209, 1995. [ bib | .pdf ] |
| [540] | Jens Palsberg and Patrick M. O'Keefe. A type system equivalent to flow analysis. ACM Transactions on Programming Languages and Systems, 17(4):576-599, July 1995. [ bib | .pdf ] |
| [541] | Jens Palsberg and Peter Ørbæk. Trust in the λ-calculus. In Static Analysis Symposium (SAS), volume 983 of Lecture Notes in Computer Science, pages 314-330, September 1995. [ bib | .dvi.gz ] |
| [542] | Jens Palsberg and Scott Smith. Constrained types and their expressiveness. ACM Transactions on Programming Languages and Systems, 18(5):519-527, September 1996. [ bib | .pdf ] |
| [543] | Jens Palsberg, Mitchell Wand, and Patrick M. O'Keefe. Type inference with non-structural subtyping. Formal Aspects of Computing, 9:49-67, 1997. [ bib | .pdf ] |
| [544] | Jens Palsberg and Tian Zhao. Efficient and flexible matching of recursive types. Information and Computation, 171:364-387, 2001. [ bib | .pdf ] |
| [545] | Jens Palsberg and Tian Zhao. Efficient type inference for record concatenation and subtyping. In IEEE Symposium on Logic in Computer Science (LICS), pages 125-136, July 2002. [ bib ] |
| [546] | Jens Palsberg and Tian Zhao. Type inference for record concatenation and subtyping. Information and Computation, 189:54-86, 2004. [ bib | .pdf ] |
| [547] | Matthew Parkinson and Gavin Bierman. Separation logic and abstraction. In ACM Symposium on Principles of Programming Languages (POPL), pages 247-258, January 2005. [ bib | .pdf ] |
| [548] | D. L. Parnas. On the criteria to be used in decomposing systems into modules. Communications of the ACM, 15(12):1053-1058, 1972. [ bib | http ] |
| [549] | Pašalić and Nathan Linger. Meta-programming with typed object-language representations. In International Conference on Generative Programming and Component Engineering (GPCE), pages 136-167, October 2004. [ bib | .ps ] |
| [550] | Emir Pašalić, Tim Sheard, and Walid Taha. DALI: An untyped, CBV functional language supporting first-order datatypes with binders (technical development). Technical Report 00-007, Oregon Graduate Institute, March 2000. [ bib | .pdf ] |
| [551] | M. S. Paterson and M. N. Wegman. Linear unification. In Annual ACM Symposium on Theory of Computing, pages 181-186, 1976. [ bib ] |
| [552] | Christine Paulin-Mohring. Extracting Fω's programs from proofs in the calculus of constructions. In ACM Symposium on Principles of Programming Languages (POPL), pages 89-104, January 1989. [ bib | http ] |
| [553] | Christine Paulin-Mohring. Inductive definitions in the system Coq: rules and properties. Research Report RR1992-49, ENS Lyon, 1992. [ bib | .ps.Z ] |
| [554] | Thomas J. Pennello. Very fast LR parsing. In Symposium on Compiler Construction, pages 145-151, 1986. [ bib | http ] |
| [555] | François Pessaux and Xavier Leroy. Type-based analysis of uncaught exceptions. ACM Transactions on Programming Languages and Systems, 22(2):340-377, 2000. [ bib | .ps.gz ] |
| [556] | John Peterson and Mark P. Jones. Implementing type classes. In ACM Conference on Programming Language Design and Implementation (PLDI), pages 227-236, June 1993. [ bib | .ps ] |
| [557] | Simon Peyton Jones. The implementation of functional programming languages. Prentice Hall, 1987. [ bib | http ] |
| [558] | Simon Peyton Jones, editor. Haskell 98 language and libraries: The revised report. Cambridge University Press, April 2003. [ bib | http ] |
| [559] | Simon Peyton Jones and Mark Shields. Lexically-scoped type variables. Manuscript, April 2004. [ bib | http ] |
| [560] | Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields. Practical type inference for arbitrary-rank types. Manuscript, July 2005. [ bib | .ps.gz ] |
| [561] | Simon Peyton Jones and Philip Wadler. Imperative functional programming. In ACM Symposium on Principles of Programming Languages (POPL), January 1993. [ bib | .ps.gz ] |
| [562] | Simon Peyton Jones, Geoffrey Washburn, and Stephanie Weirich. Wobbly types: type inference for generalised algebraic data types. Technical Report MS-CIS-05-26, University of Pennsylvania, July 2004. [ bib | .pdf ] |
| [563] | Simon L. Peyton Jones and Philip Wadler. Imperative functional programming. In ACM Symposium on Principles of Programming Languages (POPL), pages 71-84, 1993. [ bib | .ps.gz ] |
| [564] | Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In ACM Conference on Programming Language Design and Implementation (PLDI), pages 199-208, June 1988. [ bib | http ] |
| [565] | Frank Pfenning and Peter Lee. LEAP: A language with eval and polymorphism. In International Joint Conference on Theory and Practice of Software Development (TAPSOFT), volume 352 of Lecture Notes in Computer Science, pages 345-359. Springer Verlag, 1989. [ bib | http ] |
| [566] | Benjamin Pierce and Davide Sangiorgi. Typing and subtyping for mobile processes. In IEEE Symposium on Logic in Computer Science (LICS), pages 376-385, June 1993. [ bib | .ps ] |
| [567] | Benjamin C. Pierce. Bounded quantification is undecidable. Information and Computation, 112(1):131-165, July 1994. [ bib | .ps ] |
| [568] | Benjamin C. Pierce. Types and programming languages. MIT Press, 2002. [ bib | http ] |
| [569] | Benjamin C. Pierce. Types and programming languages. MIT Press, 2002. [ bib ] |
| [570] | Benjamin C. Pierce and David N. Turner. Statically typed friendly functions via partially abstract types. Technical Report ECS-LFCS-93-256, University of Edinburgh, LFCS, April 1993. Also available as INRIA Research Report 1899. [ bib | .ps ] |
| [571] | Benjamin C. Pierce and David N. Turner. Simple type-theoretic foundations for object-oriented programming. Journal of Functional Programming, 4(2):207-247, April 1994. [ bib | .ps ] |
| [572] | Benjamin C. Pierce and David N. Turner. Local type inference. ACM Transactions on Programming Languages and Systems, 22(1):1-44, January 2000. [ bib | http ] |
| [573] | Andrew M. Pitts. Parametric polymorphism and operational equivalence. Mathematical Structures in Computer Science, 10:321-359, 2000. [ bib | .pdf ] |
| [574] | Andrew M. Pitts. Nominal logic, A first order theory of names and binding. Information and Computation, 186:165-193, 2003. [ bib | .pdf ] |
| [575] | Andrew M. Pitts. Alpha-structural recursion and induction. In International Conference on Theorem Proving in Higher Order Logics (TPHOLs), Lecture Notes in Computer Science. Springer Verlag, August 2005. [ bib | .pdf ] |
| [576] | Andrew M. Pitts. Alpha-structural recursion and induction. Journal of the ACM, 53:459-506, 2006. [ bib | .pdf ] |
| [577] | Andrew M. Pitts and Murdoch J. Gabbay. A metalanguage for programming with bound names modulo renaming. In International Conference on Mathematics of Program Construction (MPC), volume 1837 of Lecture Notes in Computer Science, pages 230-255. Springer Verlag, 2000. [ bib | .pdf ] |
| [578] | Gordon Plotkin. An illative theory of relations. In Situation Theory and its Applications, number 22 in CSLI Lecture Notes, pages 133-146. Stanford University, 1990. [ bib | .pdf ] |
| [579] | Gordon D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5(3):225-255, 1977. [ bib | .pdf ] |
| [580] | François Pottier. Implémentation d'un système de modules évolué en Caml-Light. Research Report 2449, INRIA, 1995. [ bib | .ps.gz ] |
| [581] | François Pottier. Type inference and simplification for recursively constrained types. In Actes du GDR Programmation 1995 (journée du pôle Programmation Fonctionnelle), November 1995. [ bib | .ps.gz ] |
| [582] | François Pottier. Simplifying subtyping constraints. In ACM International Conference on Functional Programming (ICFP), pages 122-133, January 1996. [ bib | .ps.gz ] |
| [583] | François Pottier. A framework for type inference with subtyping. In ACM International Conference on Functional Programming (ICFP), pages 228-238, September 1998. [ bib | .ps.gz ] |
| [584] | François Pottier. Synthèse de types en présence de sous-typage: de la théorie à la pratique. PhD thesis, Université Paris 7, July 1998. [ bib | .ps.gz ] |
| [585] | François Pottier. Type inference in the presence of subtyping: from theory to practice. Research Report 3483, INRIA, September 1998. [ bib | .ps.gz ] |
| [586] | François Pottier. A 3-part type inference engine. In European Symposium on Programming (ESOP), volume 1782 of Lecture Notes in Computer Science, pages 320-335. Springer Verlag, March 2000. [ bib | .ps.gz ] |
| [587] | François Pottier. A versatile constraint-based type inference system. Nordic Journal of Computing, 7(4):312-347, November 2000. [ bib | .ps.gz ] |
| [588] | François Pottier. Wallace: an efficient implementation of type inference with subtyping, February 2000. [ bib | http ] |
| [589] | François Pottier. A semi-syntactic soundness proof for HM(X). Research Report 4150, INRIA, March 2001. [ bib | .ps.gz ] |
| [590] | François Pottier. Simplifying subtyping constraints: a theory. Information and Computation, 170(2):153-183, November 2001. [ bib | .ps.gz ] |
| [591] | François Pottier. A simple view of type-secure information flow in the π-calculus. In IEEE Computer Security Foundations Workshop, pages 320-330, June 2002. [ bib | .ps.gz ] |
| [592] | François Pottier. A constraint-based presentation and generalization of rows. In IEEE Symposium on Logic in Computer Science (LICS), pages 331-340, June 2003. [ bib | .ps.gz ] |
| [593] | François Pottier. Cαml, June 2005. [ bib | http ] |
| [594] | François Pottier. An overview of Cαml. In ACM Workshop on ML, volume 148(2) of Electronic Notes in Theoretical Computer Science, pages 27-52, March 2006. [ bib | .pdf ] |
| [595] | François Pottier. Static name control for FreshML. In IEEE Symposium on Logic in Computer Science (LICS), July 2007. To appear. [ bib | .pdf ] |
| [596] | François Pottier and Sylvain Conchon. Information flow inference for free. In ACM International Conference on Functional Programming (ICFP), pages 46-57, September 2000. [ bib | .ps.gz ] |
| [597] | François Pottier and Nadji Gauthier. Polymorphic typed defunctionalization. In ACM Symposium on Principles of Programming Languages (POPL), pages 89-98, January 2004. [ bib | .pdf ] |
| [598] | François Pottier and Nadji Gauthier. Polymorphic typed defunctionalization and concretization. Higher-Order and Symbolic Computation, 19:125-162, March 2006. [ bib | .ps.gz | .pdf ] |
| [599] | François Pottier and Yann Régis-Gianas. Stratified type inference for generalized algebraic data types. In ACM Symposium on Principles of Programming Languages (POPL), January 2006. [ bib | .pdf ] |
| [600] | François Pottier and Yann Régis-Gianas. Towards efficient, typed LR parsers. In ACM Workshop on ML, volume 148(2) of Electronic Notes in Theoretical Computer Science, pages 155-180, March 2006. [ bib | .pdf ] |
| [601] | François Pottier and Didier Rémy. The essence of ML type inference. Draft of an extended version. Unpublished, September 2003. [ bib | .ps.gz ] |
| [602] | François Pottier and Didier Rémy. The essence of ML type inference. In Benjamin C. Pierce, editor, Advanced Topics in Types and Programming Languages, chapter 10, pages 389-489. MIT Press, 2005. [ bib ] |
| [603] | François Pottier and Vincent Simonet. Information flow inference for ML. In ACM Symposium on Principles of Programming Languages (POPL), pages 319-330, January 2002. [ bib | .ps.gz ] |
| [604] | François Pottier and Vincent Simonet. Information flow inference for ML. ACM Transactions on Programming Languages and Systems, 25(1):117-158, January 2003. [ bib | .ps.gz ] |
| [605] | François Pottier, Christian Skalka, and Scott Smith. A systematic approach to static access control. In European Symposium on Programming (ESOP), volume 2028 of Lecture Notes in Computer Science, pages 30-45. Springer Verlag, April 2001. [ bib | .ps.gz ] |
| [606] | François Pottier, Christian Skalka, and Scott Smith. A systematic approach to static access control. To appear in ACM Transactions on Programming Languages and Systems, October 2003. [ bib | .ps.gz ] |
| [607] | Garrel Pottinger. A type assignment for the strongly normalizable λ-terms. In J. Roger Hindley and Jonathan P. Seldin, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pages 561-577. Academic Press, 1980. [ bib ] |
| [608] | Vaughan Pratt and Jerzy Tiuryn. Satisfiability of inequalities in a poset. Fundamenta Informaticæ, 28(1-2):165-182, 1996. [ bib | .ps.gz ] |
| [609] | William Pugh and Grant Weddell. Two-directional record layout for multiple inheritance. In ACM Conference on Programming Language Design and Implementation (PLDI), pages 85-91, 1990. [ bib | http ] |
| [610] | Zhenyu Qian. Unification of higher-order patterns in linear time and space. Journal of Logic and Computation, 6(3):315-341, 1996. [ bib ] |
| [611] | Christophe Raffalli. Type checking in system Fη. Prépublication 98-05a, LAMA, Université de Savoie, 1998. [ bib | .ps ] |
| [612] | Christophe Raffalli. An optimized complete semi-algorithm for system Fη. Unpublished, 1999. [ bib | .ps ] |
| [613] | Viswanath Ramachandran and Pascal Van Hentenryck. Incremental algorithms for constraint solving and entailment over rational trees. In Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), pages 205-217, 1993. [ bib ] |
| [614] | Franz Regensburger. HOLCF: Higher order logic of computable functions. In International Conference on Theorem Proving in Higher Order Logics (TPHOLs), volume 971 of Lecture Notes in Computer Science, pages 293-307. Springer Verlag, September 1995. [ bib | .pdf ] |
| [615] | Jakob Rehof. Minimal typings in atomic subtyping. Technical Report D-278, Department of Computer Science, University of Copenhagen, 1996. [ bib | .ps.gz ] |
| [616] | Jakob Rehof. Minimal typings in atomic subtyping. In ACM Symposium on Principles of Programming Languages (POPL), pages 278-291, January 1997. [ bib | .ps ] |
| [617] | Jakob Rehof and Manuel Fähndrich. Type-based flow analysis: From polymorphic subtyping to CFL-reachability. In ACM Symposium on Principles of Programming Languages (POPL), pages 54-66, January 2001. [ bib | .ps ] |
| [618] | Didier Rémy. Extending ML type system with a sorted equational theory. Technical Report 1766, INRIA, 1992. [ bib | .ps.gz ] |
| [619] | Didier Rémy. Projective ML. In ACM Symposium on Lisp and Functional Programming (LFP), pages 66-75, 1992. [ bib | .ps.gz ] |
| [620] | Didier Rémy. Syntactic theories and the algebra of record terms. Research Report 1869, INRIA, 1993. [ bib | .ps.gz ] |
| [621] | Didier Rémy. Programming objects with ML-ART: An extension to ML with abstract and record types. In International Symposium on Theoretical Aspects of Computer Software (TACS), pages 321-346. Springer Verlag, April 1994. [ bib | .ps.gz ] |
| [622] | Didier Rémy. Type inference for records in a natural extension of ML. In Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects Of Object-Oriented Programming. Types, Semantics and Language Design. MIT Press, 1994. [ bib | .ps.gz ] |
| [623] | Didier Rémy. Typing record concatenation for free. In Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects Of Object-Oriented Programming. Types, Semantics and Language Design. MIT Press, 1994. [ bib | .ps.gz ] |
| [624] | Didier Rémy. A case study of typechecking with constrained types: Typing record concatenation. Workshop on Advances in Types for Computer Science, August 1995. [ bib | .dvi.gz ] |
| [625] | Didier Rémy. From classes to objects via subtyping. In European Symposium on Programming (ESOP), volume 1381 of Lecture Notes in Computer Science, pages 200-220. Springer Verlag, March 1998. [ bib | .ps.gz ] |
| [626] | Didier Rémy and Jérôme Vouillon. Objective ML: A simple object-oriented extension of ML. In ACM Symposium on Principles of Programming Languages (POPL), pages 40-53, January 1997. [ bib | .ps.gz ] |
| [627] | Didier Rémy and Jérôme Vouillon. Objective ML: An effective object-oriented extension to ML. Theory and Practice of Object Systems, 4(1):27-50, 1998. [ bib | .ps.gz ] |
| [628] | Thomas Reps. Program analysis via graph reachability. Information and Software Technology, 40(11-12):701-726, 1998. [ bib | .pdf ] |
| [629] | Bernhard Reus and Jan Schwinghammer. Separation logic for higher-order store. In Computer Science Logic, volume 4207 of Lecture Notes in Computer Science, pages 575-590. Springer Verlag, September 2006. [ bib | .pdf ] |
| [630] | Dominique Revuz. Minimization of acyclic deterministic automata in linear time. Theoretical Computer Science, 92(1):181-189, 1992. [ bib ] |
| [631] | John C. Reynolds. Automatic computation of data set definitions. In Information Processing 68, volume 1, pages 456-461. North Holland, 1969. [ bib ] |
| [632] | John C. Reynolds. Towards a theory of type structure. In Colloque sur la Programmation, volume 19 of Lecture Notes in Computer Science, pages 408-425. Springer Verlag, April 1974. [ bib | http ] |
| [633] | John C. Reynolds. Syntactic control of interference. In ACM Symposium on Principles of Programming Languages (POPL), pages 39-46, January 1978. [ bib | http ] |
| [634] | John C. Reynolds. Types, abstraction and parametric polymorphism. In Information Processing 83, pages 513-523. Elsevier Science, 1983. [ bib | .pdf ] |
| [635] | John C. Reynolds. Three approaches to type structure. In International Joint Conference on Theory and Practice of Software Development (TAPSOFT), volume 185 of Lecture Notes in Computer Science, pages 97-138. Springer Verlag, March 1985. [ bib | http ] |
| [636] | John C. Reynolds. An introduction to the polymorphic lambda calculus. In Gérard Huet, editor, Logical Foundations of Functional Programming, pages 77-86. Addison-Wesley, 1990. [ bib | .ps.gz ] |
| [637] | John C. Reynolds. Definitional interpreters for higher-order programming languages. Higher-Order and Symbolic Computation, 11(4):363-397, December 1998. [ bib | .dvi.gz ] |
| [638] | John C. Reynolds. Definitional interpreters revisited. Higher-Order and Symbolic Computation, 11(4):355-361, December 1998. [ bib | .dvi.gz ] |
| [639] | John C. Reynolds. Separation logic: A logic for shared mutable data structures. In IEEE Symposium on Logic in Computer Science (LICS), pages 55-74, 2002. [ bib | .ps.gz ] |
| [640] | Morten Rhiger. A foundation for embedded languages. ACM Transactions on Programming Languages and Systems, 25(3):291-315, May 2003. [ bib | http ] |
| [641] | Michael F. Ringenburg and Dan Grossman. Types for describing coordinated data structures. In Workshop on Types in Language Design and Implementation (TLDI), pages 25-36, January 2005. [ bib | .pdf ] |
| [642] | Mikael Rittri. Using types as search keys in function libraries. Journal of Functional Programming, 1(1):71-89, 1991. [ bib ] |
| [643] | Mikael Rittri. Retrieving library functions by unifying types modulo linear isomorphism. RAIRO Theoretical Informatics and Applications, 27(6):523-540, 1993. [ bib | .ps.Z ] |
| [644] | J. Alan Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23-41, 1965. [ bib | http ] |
| [645] | John L. Ross and Mooly Sagiv. Building a bridge between pointer aliases and program dependences. Nordic Journal of Computing, 5(4):361-386, 1998. [ bib | .ps ] |
| [646] | Andreas Rossberg, Peter J. Stuckey, Martin Sulzmann, and Jeremy Wazny. The Chameleon language. [ bib | http ] |
| [647] | Colin Runciman and Ian Toyn. Retrieving re-usable software components by polymorphic type. Journal of Functional Programming, 1(2):191-211, 1991. [ bib ] |
| [648] | Claudio V. Russo. Types for modules. PhD thesis, University of Edinburgh, 1998. [ bib | .html ] |
| [649] | Didier Rémy. Type checking records and variants in a natural extension of ML. In ACM Symposium on Principles of Programming Languages (POPL), pages 77-88, 1989. [ bib | http ] |
| [650] | Didier Rémy. Efficient representation of extensible records. In ACM Workshop on ML and its Applications, June 1992. [ bib | .ps.gz ] |
| [651] | Didier Rémy. Simple, partial type inference for system F based on type containment. In ACM International Conference on Functional Programming (ICFP), September 2005. [ bib | .pdf ] |
| [652] | Didier Rémy. Simple, partial type inference for system F based on type containment. In ACM International Conference on Functional Programming (ICFP), September 2005. [ bib | .pdf ] |
| [653] | Andrei Sabelfeld and David Sands. A PER model of secure information flow in sequential programs. In European Symposium on Programming (ESOP), volume 1575 of Lecture Notes in Computer Science, pages 40-58. Springer Verlag, 1999. [ bib | .ps ] |
| [654] | Amr Sabry. What is a purely functional language? Journal of Functional Programming, 8(1):1-22, January 1998. [ bib | http ] |
| [655] | Bratin Saha, Nevin Heintze, and Dino Oliva. Subtransitive CFA using types. Technical Report YALEU/DCS/TR-1166, Yale University, October 1998. [ bib | .ps.gz ] |
| [656] | Davide Sangiorgi. On the bisimulation proof method. Mathematical Structures in Computer Science, 8(5):447-479, 1998. [ bib | .ps.gz ] |
| [657] | Patrick M. Sansom. Time profiling a lazy functional compiler. In Functional Programming, Workshops in Computing. Springer Verlag, July 1993. [ bib | .ps.gz ] |
| [658] | Fred B. Schneider. Enforceable security policies. ACM Transactions on Information and System Security, 3(1):1-50, February 2000. [ bib | .pdf ] |
| [659] | Lutz Schröder and Till Mossakowski. HasCASL: Towards integrated specification and development of functional programs. In International Conference on Algebraic Methodology and Software Technology (AMAST), volume 2422 of Lecture Notes in Computer Science, pages 99-116. Springer Verlag, September 2002. [ bib | .ps ] |
| [660] | Lenhart K. Schubert, Mary Angela Papalaskaris, and Jay Taugher. Determining type, part, color, and time relationships. Computer, 16(10):53-60, October 1983. [ bib ] |
| [661] | Michael I. Schwartzbach. Polymorphic type inference. Technical Report BRICS-LS-95-3, BRICS, June 1995. [ bib | .ps.gz ] |
| [662] | Carsten Schürmann, Adam Poswolsky, and Jeffrey Sarnat. The -calculus: Functional programming with higher-order encodings. Technical Report YALEU/DCS/TR-1272, Yale University, November 2004. [ bib | .pdf ] |
| [663] | Dana S. Scott. A type-theoretical alternative to ISWIM, CUCH, OWHY. Theoretical Computer Science, 121(1-2):411-440, 1993. [ bib | http ] |
| [664] | Robert Sedgewick and Michael Schidlowsky. Algorithms in Java: Graph algorithms. Addison-Wesley, 2003. [ bib ] |
| [665] | R. C. Sekar, R. Ramesh, and I. V. Ramakrishnan. Adaptive pattern matching. SIAM Journal on Computing, 24(6):1207-1234, December 1995. [ bib | .ps ] |
| [666] | Ravi Sethi and J. D. Ullman. The generation of optimal code for arithmetic expressions. Journal of the ACM, 17(4):715-728, 1970. [ bib | http ] |
| [667] | Peter Sewell and Jan Vitek. Secure composition of untrusted code: Wrappers and causality types. Technical Report 478, Computer Laboratory, University of Cambridge, November 1999. [ bib | .ps ] |
| [668] | Peter Sewell and Jan Vitek. Secure composition of untrusted code: Wrappers and causality types. In IEEE Computer Security Foundations Workshop, July 2000. [ bib | .ps ] |
| [669] | Edwin Hsing-Mean Sha and Kenneth Steiglitz. Maintaining bipartite matchings in the presence of failures. Networks, 23(5):459-471, August 1993. [ bib | .ps ] |
| [670] | Zhong Shao, Valery Trifonov, Bratin Saha, and Nikolaos Papaspyrou. A type system for certified binaries. ACM Transactions on Programming Languages and Systems, 27(1):1-45, 2005. [ bib | .pdf ] |
| [671] | Tim Sheard. Using MetaML: A staged programming language. In Advanced Functional Programming, volume 1608 of Lecture Notes in Computer Science, pages 207-239. Springer Verlag, September 1998. [ bib | .ps ] |
| [672] | Tim Sheard. Accomplishments and research challenges in meta-programming. In International Workshop on Semantics, Applications, and Implementation of Program Generation (SAIG), volume 2196 of Lecture Notes in Computer Science, pages 2-44. Springer Verlag, 2001. [ bib | .pdf ] |
| [673] | Tim Sheard. Languages of the future. In ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 116-119, October 2004. [ bib | http ] |
| [674] | Tim Sheard. Ωmega, November 2005. [ bib | http ] |
| [675] | Tim Sheard. Putting Curry-Howard to work. In Haskell workshop, 2005. [ bib | .ps ] |
| [676] | Tim Sheard and Emir Pašalić. Meta-programming with built-in type equality. In Workshop on Logical Frameworks and Meta-Languages (LFM), July 2004. [ bib | .pdf ] |
| [677] | Mark B. Shields and Simon Peyton Jones. First class modules for Haskell. In Workshop on Foundations of Object-Oriented Languages (FOOL), pages 28-40, January 2002. [ bib | .pdf ] |
| [678] | Mark R. Shinwell. The fresh approach: functional programming with names and binders. PhD thesis, University of Cambridge, February 2005. [ bib | .pdf ] |
| [679] | Mark R. Shinwell. Fresh O'Caml: nominal abstract syntax for the masses. In ACM Workshop on ML, September 2005. [ bib | .pdf ] |
| [680] | Mark R. Shinwell and Andrew M. Pitts. Fresh Objective Caml user manual. Technical Report 621, University of Cambridge, February 2005. [ bib | .pdf ] |
| [681] | Mark R. Shinwell and Andrew M. Pitts. On a monadic semantics for freshness. Theoretical Computer Science, 342:28-55, 2005. [ bib | .pdf ] |
| [682] | Mark R. Shinwell, Andrew M. Pitts, and Murdoch J. Gabbay. FreshML: Programming with binders made simple. In ACM International Conference on Functional Programming (ICFP), pages 263-274, August 2003. [ bib | .pdf ] |
| [683] | Olin Shivers. A universal scripting framework or, Lambda: the ultimate “little language”. In Concurrency and Parallelism: Programming, Networking and Security, volume 1179 of Lecture Notes in Computer Science, pages 254-265. Springer Verlag, 1996. [ bib | .ps ] |
| [684] | Vincent Simonet. Fine-grained information flow analysis for a λ-calculus with sum types. In IEEE Computer Security Foundations Workshop, pages 223-237, June 2002. [ bib | .ps.gz ] |
| [685] | Vincent Simonet. An extension of HM(X) with bounded existential and universal data-types. In ACM International Conference on Functional Programming (ICFP), June 2003. [ bib | .ps.gz ] |
| [686] | Vincent Simonet. The Flow Caml system: documentation and user's manual. Technical Report 0282, INRIA, July 2003. [ bib | http ] |
| [687] | Vincent Simonet. Type inference with structural subtyping: a faithful formalization of an efficient constraint solver. In Asian Symposium on Programming Languages and Systems (APLAS), volume 2895 of Lecture Notes in Computer Science. Springer Verlag, November 2003. [ bib | .pdf ] |
| [688] | Vincent Simonet. Inférence de flots d'information pour ML: formalisation et implantation. PhD thesis, Université Paris 7, March 2004. [ bib | .pdf ] |
| [689] | Vincent Simonet and François Pottier. Constraint-based type inference for guarded algebraic data types. Research Report 5462, INRIA, January 2005. [ bib | .html ] |
| [690] | Christian Skalka. Types for programming language-based security. PhD thesis, The Johns Hopkins University, August 2002. [ bib | .ps ] |
| [691] | Christian Skalka and François Pottier. Syntactic type soundness for HM(X). In Workshop on Types in Programming (TIP), volume 75 of Electronic Notes in Theoretical Computer Science, July 2002. [ bib | .ps.gz ] |
| [692] | Christian Skalka and Scott Smith. Static enforcement of security with types. In ACM International Conference on Functional Programming (ICFP), pages 34-45, September 2000. [ bib | .ps ] |
| [693] | Frederick Smith, David Walker, and Greg Morrisett. Alias types. In European Symposium on Programming (ESOP), volume 1782 of Lecture Notes in Computer Science, pages 366-381. Springer Verlag, March 2000. [ bib | .pdf ] |
| [694] | Geoffrey Smith and Dennis Volpano. Secure information flow in a multi-threaded imperative language. In ACM Symposium on Principles of Programming Languages (POPL), pages 355-364, January 1998. [ bib | .ps.Z ] |
| [695] | Geoffrey S. Smith. Polymorphic type inference with overloading and subtyping. In International Joint Conference on Theory and Practice of Software Development (TAPSOFT), volume 668 of Lecture Notes in Computer Science, pages 671-685. Springer Verlag, April 1993. [ bib | http ] |
| [696] | Geoffrey S. Smith. Principal type schemes for functional programs with overloading and subtyping. Science of Computer Programming, 23(2-3):197-226, December 1994. [ bib | .pdf ] |
| [697] | Geoffrey S. Smith. A new type system for secure information flow. In IEEE Computer Security Foundations Workshop, pages 115-125, June 2001. [ bib | .pdf ] |
| [698] | Scott Smith and Tiejun Wang. Polyvariant flow analysis with constrained types. In European Symposium on Programming (ESOP), volume 1782 of Lecture Notes in Computer Science, pages 382-396. Springer Verlag, March 2000. [ bib | .pdf ] |
| [699] | Scott Fraser Smith. Partial objects in type theory. PhD thesis, Cornell University, January 1989. [ bib | .pdf ] |
| [700] | Gert Smolka and Ralf Treinen. Records for logic programming. Journal of Logic Programming, 18(3):229-258, April 1994. [ bib | .ps ] |
| [701] | Alan Snyder. Encapsulation and inheritance in object-oriented programming languages. In ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 38-45, 1986. [ bib | http ] |
| [702] | Jonathan Sobel and Daniel P. Friedman. Recycling continuations. In ACM International Conference on Functional Programming (ICFP), pages 251-260, September 1998. [ bib | .ps ] |
| [703] | Marvin Solomon. Type definitions with parameters. In ACM Symposium on Principles of Programming Languages (POPL), pages 31-38, 1978. [ bib | http ] |
| [704] | Sergei V. Soloviev. The category of finite sets and cartesian closed categories. Journal of Soviet Mathematics, 22(3):1387-1400, 1983. [ bib ] |
| [705] | Matthieu Sozeau. Subset coercions in Coq. In TYPES, 2006. [ bib | .pdf ] |
| [706] | Mike Spivey. A functional theory of exceptions. Science of Computer Programming, 14:25-42, 1990. [ bib ] |
| [707] | R. Stata and M. Abadi. A type system for Java bytecode subroutines. In ACM Symposium on Principles of Programming Languages (POPL), pages 149-160, January 1998. [ bib | .html ] |
| [708] | Bjarne Steensgaard. Points-to analysis in almost linear time. In ACM Symposium on Principles of Programming Languages (POPL), pages 32-41, January 1996. [ bib | .ps ] |
| [709] | Bernhard Steffen, Andreas Claßen, Marion Klein, Jens Knoop, and Tiziana Margaria. The fixpoint-analysis machine. In International Conference on Concurrency Theory (CONCUR), volume 962 of Lecture Notes in Computer Science, pages 72-87. Springer Verlag, August 1995. [ bib | http ] |
| [710] | Mark-Oliver Stehr. CINNI - A generic calculus of explicit substitutions and its application to λ-, σ- and π-calculi. In International Workshop on Rewriting Logic and its Applications (WRLA), volume 36 of Electronic Notes in Theoretical Computer Science. Elsevier Science, September 2000. [ bib | .ps ] |
| [711] | Allen Stoughton. Access flow: A protection model which integrates access control and information flow. In IEEE Symposium on Security and Privacy (S&P), pages 9-18, 1981. [ bib ] |
| [712] | Christopher Strachey. Fundamental concepts in programming languages. Higher-Order and Symbolic Computation, 13(1-2):11-49, April 2000. [ bib | http ] |
| [713] | Peter J. Stuckey and Martin Sulzmann. A theory of overloading. In ACM International Conference on Functional Programming (ICFP), pages 167-178, 2002. [ bib | .ps.gz ] |
| [714] | Peter J. Stuckey and Martin Sulzmann. Type inference for guarded recursive data types. Manuscript, February 2005. [ bib | .ps.gz ] |
| [715] | Peter J. Stuckey, Martin Sulzmann, and Jeremy Wazny. Interactive type debugging in Haskell. In Haskell workshop, pages 72-83, 2003. [ bib | .ps.gz ] |
| [716] | Zhendong Su and Alexander Aiken. Entailment with conditional equality constraints. In European Symposium on Programming (ESOP), volume 2028 of Lecture Notes in Computer Science, pages 170-189, April 2001. [ bib | .pdf ] |
| [717] | Zhendong Su, Alexander Aiken, Joachim Niehren, Tim Priesnitz, and Ralf Treinen. The first-order theory of subtyping constraints. In ACM Symposium on Principles of Programming Languages (POPL), pages 203-216, January 2002. [ bib | .pdf ] |
| [718] | Martin Sulzmann. Designing record systems. Research Report YALEU/DCS/RR-1128, Yale University, April 1997. [ bib | .ps.gz ] |
| [719] | Martin Sulzmann. Completenss of constraint-based inference. October 2000. [ bib | .ps ] |
| [720] | Martin Sulzmann. A general framework for Hindley/Milner type systems with constraints. PhD thesis, Yale University, Department of Computer Science, May 2000. [ bib | .ps.gz ] |
| [721] | Martin Sulzmann. A general type inference framework for Hindley/Milner style systems. In International Symposium on Functional and Logic Programming, volume 2024 of Lecture Notes in Computer Science, pages 246-263. Springer Verlag, March 2001. [ bib | .pdf ] |
| [722] | Martin Sulzmann, Martin Müller, and Christoph Zenger. Hindley/Milner style type systems in constraint form. Research Report ACRC-99-009, University of South Australia, School of Computer and Information Science, July 1999. [ bib | .ps.gz ] |
| [723] | Martin Sulzmann, Martin Odersky, and Martin Wehr. Type inference with constrained types. In Workshop on Foundations of Object-Oriented Languages (FOOL), January 1997. [ bib | .ps.gz ] |
| [724] | Martin Sulzmann and Meng Wang. A systematic translation of guarded recursive data types to existential types. Technical Report TR22/04, National University of Singapore, 2004. [ bib | .ps.gz ] |
| [725] | Martin Sulzmann, Jeremy Wazny, and Peter J. Stuckey. A framework for extended algebraic data types. Manuscript, July 2005. [ bib | .pdf ] |
| [726] | Eijiro Sumii and Naoki Kobayashi. A generalized deadlock-free process calculus. In International Workshop on High-Level Concurrent Languages (HLCL), volume 16 of Electronic Notes in Theoretical Computer Science, pages 55-77. Elsevier Science, September 1998. [ bib | .ps ] |
| [727] | Nikhil Swamy, Michael Hicks, Greg Morrisett, Dan Grossman, and Trevor Jim. Safe manual memory management in Cyclone. Science of Computer Programming, 62(2):122-144, October 2006. [ bib | .pdf ] |
| [728] | Walid Taha and Michael Florentin Nielsen. Environment classifiers. In ACM Symposium on Principles of Programming Languages (POPL), pages 26-37, January 2003. [ bib | .pdf ] |
| [729] | Carolyn Talcott. A theory of binding structures and applications to rewriting. Theoretical Computer Science, 112(1):99-143, 1993. [ bib | .ps.Z ] |
| [730] | David R. Tarditi and Andrew W. Appel. ML-Yacc user's manual, April 2000. [ bib | http ] |
| [731] | Robert Tarjan. Depth-first search and linear graph algorithms. SIAM Journal on Computing, 1(2):146-160, June 1972. [ bib | .pdf ] |
| [732] | Robert Endre Tarjan. Efficiency of a good but not linear set union algorithm. Journal of the ACM, 22(2):215-225, April 1975. [ bib ] |
| [733] | Robert Endre Tarjan. Applications of path compression on balanced trees. Journal of the ACM, 26(4):690-715, October 1979. [ bib | http ] |
| [734] | Robert Endre Tarjan. Amortized computational complexity. SIAM Journal on Algebraic and Discrete Methods, 6(2):306-318, 1985. [ bib | http ] |
| [735] | The GHC team. The Glasgow Haskell compiler, March 2005. [ bib | http ] |
| [736] | Satish R. Thatté. Automated synthesis of interface adapters for reusable classes. In ACM Symposium on Principles of Programming Languages (POPL), pages 174-187, January 1994. [ bib | http ] |
| [737] | The Coq development team. The Coq proof assistant, 2006. [ bib | http ] |
| [738] | Hayo Thielecke. Frame rules from answer types for code pointers. In ACM Symposium on Principles of Programming Languages (POPL), pages 309-319, January 2006. [ bib | .pdf ] |
| [739] | Peter Thiemann. ML-style typing, lambda lifting, and partial evaluation. In Latin American Conference on Functional Programming, March 1999. [ bib | .ps.gz ] |
| [740] | Peter Thiemann. Enforcing security properties using type specialization. In European Symposium on Programming (ESOP), Lecture Notes in Computer Science. Springer Verlag, April 2001. [ bib | .ps.gz ] |
| [741] | Jerzy Tiuryn. Subtype inequalities. In IEEE Symposium on Logic in Computer Science (LICS), pages 308-317, June 1992. [ bib ] |
| [742] | Jerzy Tiuryn and Mitchell Wand. Type reconstruction with recursive types and atomic subtyping. In International Joint Conference on Theory and Practice of Software Development (TAPSOFT), volume 668 of Lecture Notes in Computer Science, pages 686-701. Springer Verlag, April 1993. [ bib | .dvi ] |
| [743] | Mads Tofte. Operational semantics and polymorphic type inference. PhD thesis, University of Edinburgh, 1988. [ bib | .ps ] |
| [744] | Mads Tofte, Lars Birkedal, Martin Elsman, and Niels Hallenberg. A retrospective on region-based memory management. Higher-Order and Symbolic Computation, 17(3):245-265, September 2004. [ bib | .ps.gz ] |
| [745] | Mads Tofte and Jean-Pierre Talpin. Implementation of the typed call-by-value λ-calculus using a stack of regions. In ACM Symposium on Principles of Programming Languages (POPL), pages 188-201, January 1994. [ bib | .pdf ] |
| [746] | Mads Tofte and Jean-Pierre Talpin. Region-based memory management. Information and Computation, 132(2):109-176, 1997. [ bib | .pdf ] |
| [747] | Andrew Tolmach. Combining closure conversion with closure analysis using algebraic types. In Workshop on Types in Compilation (TIC), June 1997. [ bib | .ps ] |
| [748] | Andrew Tolmach and Dino P. Oliva. From ML to Ada: Strongly-typed language interoperability via source translation. Journal of Functional Programming, 8(4):367-412, July 1998. [ bib | http ] |
| [749] | Valery Trifonov and Scott Smith. Subtyping constrained types. In Static Analysis Symposium (SAS), volume 1145 of Lecture Notes in Computer Science, pages 349-365. Springer Verlag, September 1996. [ bib | .pdf ] |
| [750] | Stephen Tse and Steve Zdancewic. Run-time principals in information-flow type systems. In IEEE Symposium on Security and Privacy (S&P), May 2004. [ bib | .pdf ] |
| [751] | Hideki Tsuiki. On typed calculi with a merge operator. In Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), volume 880 of Lecture Notes in Computer Science, pages 101-112. Springer Verlag, 1994. [ bib | .ps.gz ] |
| [752] | David N. Turner. The polymorphic pi-calculus: Theory and implementation. PhD thesis, University of Edinburgh, 1995. [ bib | http ] |
| [753] | David N. Turner, Philip Wadler, and Christian Mossin. Once upon a type. In Conference on Functional Programming Languages and Computer Architecture (FPCA), pages 1-11. ACM Press, June 1995. [ bib | .dvi ] |
| [754] | Christian Urban, Andrew Pitts, and Murdoch Gabbay. Nominal unification. Theoretical Computer Science, 323:473-497, 2004. [ bib | .ps ] |
| [755] | Christian Urban and Christine Tasson. Nominal techniques in Isabelle/HOL. In International Conference on Automated Deduction (CADE), Lecture Notes in Computer Science. Springer Verlag, 2005. [ bib | .ps ] |
| [756] | Vincent van Oostrom. Confluence by decreasing diagrams. Theoretical Computer Science, 126(2):259-280, April 1994. [ bib | .ps.Z ] |
| [757] | Eric van Wyk, Oege de Moor, and Simon Peyton Jones. Aspect-oriented compilers. In Generative and Component-Based Software Engineering, volume 1799 of Lecture Notes in Computer Science, pages 121-133. Springer Verlag, September 1999. [ bib | .ps.gz ] |
| [758] | Mandana Vaziri and Daniel Jackson. Checking heap-manipulating procedures with a constraint solver. In International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), volume 2619 of Lecture Notes in Computer Science. Springer Verlag, April 2003. [ bib | .pdf ] |
| [759] | B. Vergauwen, J. Wauman, and J. Lewi. Efficient fixpoint computation. In Static Analysis Symposium (SAS), volume 864 of Lecture Notes in Computer Science, pages 314-328. Springer Verlag, 1994. [ bib | http ] |
| [760] | Dennis Volpano. Provably-secure programming languages for remote evaluation. ACM SIGPLAN Notices, 32(1):117-119, January 1997. [ bib ] |
| [761] | Dennis Volpano and Geoffrey Smith. Eliminating covert flows with minimum typings. In IEEE Computer Security Foundations Workshop, pages 156-168, June 1997. [ bib | .ps.Z ] |
| [762] | Dennis Volpano and Geoffrey Smith. A type-based approach to program security. Lecture Notes in Computer Science, 1214:607-621, April 1997. [ bib | .ps.Z ] |
| [763] | Dennis Volpano, Geoffrey Smith, and Cynthia Irvine. A sound type system for secure flow analysis. Journal of Computer Security, 4(3):167-187, 1996. [ bib | .ps.Z ] |
| [764] | Sergei G. Vorobyov. An improved lower bound for the elementary theories of trees. In International Conference on Automated Deduction (CADE), volume 1104 of Lecture Notes in Computer Science, pages 275-287. Springer Verlag, 1996. [ bib | .ps.Z ] |
| [765] | Dimitrios Vytiniotis and Stephanie Weirich. Dependent types: Easy as PIE. In Trends in Functional Programming (TFP), April 2007. [ bib | .pdf ] |
| [766] | Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones. Boxy types: type inference for higher-rank types and impredicativity. Manuscript, April 2005. [ bib | http ] |
| [767] | Philip Wadler. Theorems for free! In Conference on Functional Programming Languages and Computer Architecture (FPCA), pages 347-359, September 1989. [ bib | .ps.gz ] |
| [768] | Philip Wadler. Linear types can change the world! In M. Broy and C. Jones, editors, Programming Concepts and Methods. North Holland, April 1990. [ bib | .ps ] |
| [769] | Philip Wadler. Comprehending monads. Mathematical Structures in Computer Science, 2:461-493, 1992. [ bib | .ps.gz ] |
| [770] | Philip Wadler. The essence of functional programming. In ACM Symposium on Principles of Programming Languages (POPL), pages 1-14, 1992. Invited talk. [ bib | .ps ] |
| [771] | Philip Wadler. The Girard-Reynolds isomorphism (second edition). Theoretical Computer Science, 375(1-3):201-226, May 2007. [ bib | .pdf ] |
| [772] | Philip Wadler and Stephen Blott. How to make ad-hoc polymorphism less ad-hoc. In ACM Symposium on Principles of Programming Languages (POPL), pages 60-76, January 1989. [ bib | .ps.gz ] |
| [773] | Philip Wadler and Peter Thiemann. The marriage of effects and monads. ACM Transactions on Computational Logic, 4(1):1-32, January 2003. [ bib | .ps.gz ] |
| [774] | Philip L. Wadler. How to replace failure by a list of successes. In Conference on Functional Programming Languages and Computer Architecture (FPCA), volume 201 of Lecture Notes in Computer Science, pages 113-128. Springer Verlag, September 1985. [ bib | http ] |
| [775] | David Walker. A type system for expressive security policies. In ACM Symposium on Principles of Programming Languages (POPL), pages 254-267, January 2000. [ bib | http ] |
| [776] | David Walker. Substructural type systems. In Benjamin C. Pierce, editor, Advanced Topics in Types and Programming Languages, chapter 1, pages 3-43. MIT Press, 2005. [ bib ] |
| [777] | David Walker and Greg Morrisett. Alias types for recursive data structures. In Workshop on Types in Compilation (TIC), volume 2071 of Lecture Notes in Computer Science, pages 177-206. Springer Verlag, September 2000. [ bib | .pdf ] |
| [778] | Dan S. Wallach. A new approach to mobile code security. PhD thesis, Princeton University, January 1999. [ bib | .html ] |
| [779] | Dan S. Wallach, Andrew W. Appel, and Edward W. Felten. Safkasi: A security mechanism for language-based systems. ACM Transactions on Software Engineering and Methodology, 9(4):341-378, October 2000. [ bib | .ps ] |
| [780] | Dan S. Wallach and Edward Felten. Understanding Java stack inspection. In IEEE Symposium on Security and Privacy (S&P), May 1998. [ bib | http ] |
| [781] | Mitchell Wand. Embedding type structure in semantics. In ACM Symposium on Principles of Programming Languages (POPL), pages 1-6, January 1985. [ bib | http ] |
| [782] | Mitchell Wand. Finding the source of type errors. In ACM Symposium on Principles of Programming Languages (POPL), pages 38-43, January 1986. [ bib | http ] |
| [783] | Mitchell Wand. A simple algorithm and proof for type inference. Fundamenta Informaticæ, 10:115-122, 1987. [ bib | .dvi ] |
| [784] | Mitchell Wand. Type inference for record concatenation and multiple inheritance. Information and Computation, 93(1):1-15, July 1991. [ bib | .dvi ] |
| [785] | Mitchell Wand. Type inference for objects with instance variables and inheritance. In Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design, pages 97-120. MIT Press, 1994. [ bib | .dvi ] |
| [786] | Martin Ward. Derivation of data intensive algorithms by formal transformation - the Schorr-Waite graph marking algorithm. IEEE Transactions on Software Engineering, 22(9):665-686, September 1996. [ bib | .pdf ] |
| [787] | D. H. D. Warren. Higher-order extensions to PROLOG: are they needed? In J. E. Hayes, D. Michie, and Y-H. Pao, editors, Machine Intelligence 10, pages 441-454. Ellis Horwood, 1982. [ bib ] |
| [788] | Stephanie Weirich. Type-safe cast: Functional pearl. In ACM International Conference on Functional Programming (ICFP), pages 58-67, September 2000. [ bib | .pdf ] |
| [789] | Stephanie Weirich. A typechecker that produces a typed term from an untyped source. Part of the Glasgow Haskell compiler's test suite, September 2004. [ bib | http ] |
| [790] | J. B. Wells. Typability and type checking in system F are equivalent and undecidable. Annals of Pure and Applied Logic, 98(1-3):111-156, 1999. [ bib | .ps.gz ] |
| [791] | J. B. Wells. The essence of principal typings. In International Colloquium on Automata, Languages and Programming, volume 2380 of Lecture Notes in Computer Science, pages 913-925. Springer Verlag, 2002. [ bib | .pdf ] |
| [792] | Benjamin Werner. Une théorie des constructions inductives. PhD thesis, Université Paris 7, 1994. [ bib ] |
| [793] | Edwin Westbrook, Aaron Stump, and Ian Wehrman. A language-based approach to functionally correct imperative programming. In ACM International Conference on Functional Programming (ICFP), pages 268-279, 2005. [ bib | .pdf ] |
| [794] | J. W. J. Williams. Algorithm 232: Heapsort. Communications of the ACM, 7(6):347-348, June 1964. [ bib | http ] |
| [795] | Jeannette M. Wing, Eugene Rollins, and Amy Moormann Zaremski. Thoughts on a Larch/ML and a new application for LP. In First International Workshop on Larch, pages 297-312, July 1992. [ bib | .ps ] |
| [796] | J. P. L. Woodward. Applications for multilevel secure operating systems. In Proceedings NCC, volume 48, pages 319-328. AFIPS Press, June 1979. [ bib ] |
| [797] | Andrew K. Wright. Polymorphism for imperative languages without imperative types. Technical Report 93-200, Rice University, February 1993. [ bib ] |
| [798] | Andrew K. Wright. Simple imperative polymorphism. Lisp and Symbolic Computation, 8(4):343-356, December 1995. [ bib | .ps.gz ] |
| [799] | Andrew K. Wright and Robert Cartwright. A practical soft type system for Scheme. ACM Transactions on Programming Languages and Systems, 19(1):87-152, January 1997. [ bib | http ] |
| [800] | Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38-94, November 1994. [ bib | .ps.gz ] |
| [801] | Hongwei Xi. Dependent types in practical programming. PhD thesis, Carnegie Mellon University, December 1998. [ bib | .ps ] |
| [802] | Hongwei Xi. Dead code elimination through dependent types. In International Workshop on Practical Aspects of Declarative Languages (PADL), volume 1551 of Lecture Notes in Computer Science, pages 228-242. Springer Verlag, January 1999. [ bib | .ps ] |
| [803] | Hongwei Xi. Dependent ML, 2001. [ bib | .html ] |
| [804] | Hongwei Xi. Dependently Typed Pattern Matching. Journal of Universal Computer Science, 9(8):851-872, 2003. [ bib | .pdf ] |
| [805] | Hongwei Xi. Applied type system. In TYPES 2003, volume 3085 of Lecture Notes in Computer Science, pages 394-408. Springer Verlag, February 2004. [ bib | .pdf ] |
| [806] | Hongwei Xi, Chiyan Chen, and Gang Chen. Guarded recursive datatype constructors. July 2002. [ bib | .pdf ] |
| [807] | Hongwei Xi, Chiyan Chen, and Gang Chen. Guarded recursive datatype constructors. In ACM Symposium on Principles of Programming Languages (POPL), pages 224-235, January 2003. [ bib | .ps ] |
| [808] | Hongwei Xi and Frank Pfenning. Dependent types in practical programming. In ACM Symposium on Principles of Programming Languages (POPL), pages 214-227, January 1999. [ bib | .ps ] |
| [809] | Hongwei Xi and Carsten Schürmann. CPS transform for Dependent ML. In Workshop on Logic, Language, Information and Computation (WoLLIC), August 2001. [ bib | .pdf ] |
| [810] | Yichen Xie and Alex Aiken. Scalable error detection using Boolean satisfiability. In ACM Symposium on Principles of Programming Languages (POPL), pages 351-363, January 2005. [ bib | .pdf ] |
| [811] | Dana N. Xu. Extended static checking for Haskell. In Haskell workshop, pages 48-59. ACM Press, 2006. [ bib | .ps ] |
| [812] | Nobuko Yoshida. Graph types for monadic mobile processes. In Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), volume 1180 of Lecture Notes in Computer Science, pages 371-386. Springer Verlag, 1996. [ bib | .ps.gz ] |
| [813] | Nobuko Yoshida. Graph types for monadic mobile processes. Technical Report ECS-LFCS-96-350, University of Edinburgh, 1996. [ bib | http ] |
| [814] | Nobuko Yoshida, Kohei Honda, and Martin Berger. Linearity and bisimulation. Technical Report MSC-2001/48, University of Leicester, December 2001. [ bib | .ps.gz ] |
| [815] | Nobuko Yoshida, Kohei Honda, and Martin Berger. Linearity and bisimulation. In International Conference on Foundations of Software Science and Computation Structures (FOSSACS), Lecture Notes in Computer Science. Springer Verlag, April 2002. [ bib | .ps.gz ] |
| [816] | Nobuko Yoshida, Kohei Honda, and Martin Berger. Logical reasoning for higher-order functions with local state. In International Conference on Foundations of Software Science and Computation Structures (FOSSACS), volume 4423 of Lecture Notes in Computer Science, pages 361-377. Springer Verlag, April 2007. [ bib | .pdf ] |
| [817] | Steve Zdancewic and Andrew C. Myers. Secure information flow and CPS. In European Symposium on Programming (ESOP), Lecture Notes in Computer Science. Springer Verlag, April 2001. [ bib | .ps ] |
| [818] | Steve Zdancewic and Andrew C. Myers. Secure information flow via linear continuations. Higher Order and Symbolic Computation, 15(2-3):209-234, September 2002. [ bib | .pdf ] |
| [819] | Olivier Zendra, Dominique Colnet, and Suzanne Collin. Efficient dynamic dispatch without virtual function tables. the SmallEiffel compiler. In ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 125-141, October 1997. [ bib | .ps.gz ] |
| [820] | Christoph Zenger. Indexed types. Theoretical Computer Science, 187(1-2):147-165, 1997. [ bib | http ] |
| [821] | Christoph Zenger. Indizierte typen. PhD thesis, Universität Karlsruhe, July 1998. [ bib | .ps.gz ] |
| [822] | Lantian Zheng and Andrew C. Myers. Dynamic security labels and noninterference. Technical Report 2004-1924, Cornell University, January 2004. [ bib | .pdf ] |
| [823] | Dengping Zhu and Hongwei Xi. A typeful and tagless representation for XML documents. In Asian Symposium on Programming Languages and Systems (APLAS), volume 2895 of Lecture Notes in Computer Science, pages 89-104. Springer Verlag, November 2003. [ bib | .pdf ] |
| [824] | Dengping Zhu and Hongwei Xi. Safe programming with pointers through stateful views. In International Workshop on Practical Aspects of Declarative Languages (PADL), volume 3350 of Lecture Notes in Computer Science, pages 83-97. Springer Verlag, January 2005. [ bib | .pdf ] |
| [825] | Yoav Zibin and Yossi Gil. Theory and practice of incremental subtyping tests and message dispatching, December 2001. [ bib | .ps.gz ] |
| [826] | Yoav Zibin and Yossi Gil. Fast algorithm for creating space efficient dispatching tables with application to multi-dispatching. In ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 142-160, November 2002. [ bib | .pdf ] |
| [827] | Yoav Zibin and Yossi Gil. Incremental algorithms for dispatching in dynamically typed languages. In ACM Symposium on Principles of Programming Languages (POPL), January 2003. [ bib | .pdf ] |
| [828] | Jan Zwanenburg. A type system for record concatenation and subtyping. Technical report, Eindhoven University of Technology, July 1997. [ bib | .ps ] |
This file has been generated by bibtex2html 1.85.
