[1] | Unicon. http://unicon.sourceforge.net/. [ bib | http ] |
[2] | 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 ] |
[3] | 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 ] |
[4] | Martín Abadi and Marcelo P. Fiore. Syntactic considerations on recursive types. In Logic in Computer Science (LICS), pages 242--252, July 1996. [ bib | .ps ] |
[5] | Martín Abadi, Anindya Banerjee, Nevin Heintze, and Jon G. Riecke. A core calculus of dependency. In Principles of Programming Languages (POPL), pages 147--160, January 1999. [ bib | .ps ] |
[6] | Martín Abadi and Bruno Blanchet. Secrecy types for asymmetric communication. In Foundations of Software Science and Computation Structures (FOSSACS), volume 2030 of Lecture Notes in Computer Science, pages 25--41. Springer, April 2001. [ bib | .html ] |
[7] | Martín Abadi, Butler Lampson, and Jean-Jacques Lévy. Analysis and caching of dependencies. In International Conference on Functional Programming (ICFP), pages 83--91, May 1996. [ bib | .ps ] |
[8] | 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 ] |
[9] | Andreas Abel. Termination checking with types. RAIRO Theoretical Informatics and Applications, 38(4):277--319, 2004. [ bib | .pdf ] |
[10] | Andreas Abel. MiniAgda: Integrating sized and dependent types. In Workshop on Partiality And Recursion in Interactive Theorem Provers (PAR), July 2010. [ bib | .pdf ] |
[11] | 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 ] |
[12] | Samson Abramsky. Domain theory in logical form. Annals of Pure and Applied Logic, 51:1--77, 1991. [ bib | .ps.gz ] |
[13] | Samson Abramsky, Kohei Honda, and Guy McCusker. A fully abstract game semantics for general references. In Logic in Computer Science (LICS), pages 334--344, 1998. [ bib | .ps.gz ] |
[14] | Peter Achten and Marinus J. Plasmeijer. The ins and outs of Clean I/O. Journal of Functional Programming, 5(1):81--110, 1995. [ bib | http ] |
[15] | Reynald Affeldt, Cyril Cohen, and Damien Rouhling. Formalization techniques for asymptotic reasoning in classical analysis. Journal of Formalized Reasoning, 11(1):43--76, 2018. [ bib | .pdf ] |
[16] | Sten Agerholm. A HOL basis for reasoning about functional programs. Technical Report RS-94-44, BRICS, December 1994. [ bib | .ps.gz ] |
[17] | Sten Agerholm. LCF examples in HOL. Technical Report RS-94-18, BRICS, June 1994. [ bib | .ps.gz ] |
[18] | Amal Ahmed, Andrew W. Appel, Christopher D. Richards, Kedar N. Swadi, Gang Tan, and Daniel C. Wang. Semantic foundations for typed assembly languages. ACM Transactions on Programming Languages and Systems, 32(3), 2010. [ bib | .pdf ] |
[19] | Amal Ahmed and Matthias Blume. Typed closure conversion preserves observational equivalence. In International Conference on Functional Programming (ICFP), pages 157--168, September 2008. [ bib | .pdf ] |
[20] | Amal Ahmed, Derek Dreyer, and Andreas Rossberg. State-dependent representation independence. In Principles of Programming Languages (POPL), pages 340--353, January 2009. [ bib | .pdf ] |
[21] | Amal Ahmed, Matthew Fluet, and Greg Morrisett. L^{3}: A linear language with locations. Fundamenta Informaticæ, 77(4):397--449, 2007. [ bib | .pdf ] |
[22] | Amal J. Ahmed, Andrew W. Appel, and Roberto Virga. A stratified semantics of general references embeddable in higher-order logic. In Logic in Computer Science (LICS), pages 75--86, July 2002. [ bib | .pdf ] |
[23] | Amal J. Ahmed, Matthew Fluet, and Greg Morrisett. A step-indexed model of substructural state. In International Conference on Functional Programming (ICFP), pages 78--91, September 2005. [ bib | .pdf ] |
[24] | Amal Jamil Ahmed. Semantics of types for mutable state. PhD thesis, Princeton University, 2004. [ bib | .pdf ] |
[25] | Alfred Aho, Ravi Sethi, and Jeffrey Ullman. Compilateurs: principes, techniques et outils. InterEditions, 1989. [ bib ] |
[26] | Alfred V. Aho, John E. Hopcroft, and Jeffrey D. Ullman. The design and analysis of computer algorithms. Addison-Wesley, 1974. [ bib ] |
[27] | Alfred V. Aho, John E. Hopcroft, and Jeffrey D. Ullman. Data structures and algorithms. Addison-Wesley, 1983. [ bib ] |
[28] | Alfred V. Aho, Ravi Sethi, and Jeffrey D. Ullman. Compilers: Principles, techniques, and tools. Addison-Wesley, 1986. [ bib ] |
[29] | Alfred V. Aho and Jeffrey D. Ullman. Optimization of LR(k) parsers. Journal of Computer and System Sciences, 6(6):573--602, 1972. [ bib | http ] |
[30] | Alfred V. Aho and Jeffrey D. Ullman. The theory of parsing, translation, and compiling. Prentice Hall, 1972. [ bib | http ] |
[31] | Alfred V. Aho and Jeffrey D. Ullman. A technique for speeding up LR(k) parsers. SIAM Journal on Computing, 2(2):106--127, 1973. [ bib | http ] |
[32] | Alexander Aiken. Introduction to set constraint-based program analysis. Science of Computer Programming, 35:79--111, 1999. [ bib | .pdf ] |
[33] | 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 | .pdf ] |
[34] | 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 | .pdf ] |
[35] | Alexander S. Aiken. The Illyria system, 1994. [ bib | .html ] |
[36] | 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 | .pdf ] |
[37] | Alexander S. Aiken and Manuel Fähndrich. Subtyping polymorphic constrained types. Technical Report CSD-96-898, University of California, Berkeley, March 1996. [ bib ] |
[38] | 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 | .pdf ] |
[39] | Alexander S. Aiken and Edward L. Wimmers. Solving systems of set constraints. In Logic in Computer Science (LICS), pages 329--340, June 1992. [ bib | .pdf ] |
[40] | Alexander S. Aiken and Edward L. Wimmers. Type inclusion constraints and type inference. In Functional Programming Languages and Computer Architecture (FPCA), pages 31--41. ACM Press, 1993. [ bib | .pdf ] |
[41] | Alexander S. Aiken, Edward L. Wimmers, and T. K. Lakshman. Soft typing with conditional types. In Principles of Programming Languages (POPL), pages 163--173, January 1994. [ bib | .pdf ] |
[42] | 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 | .pdf ] |
[43] | Elvira Albert, Puri Arenas, Samir Genaim, German Puebla, and Damiano Zanardini. Cost analysis of object-oriented bytecode programs. Theoretical Computer Science, 413(1):142--159, 2012. [ bib | .pdf ] |
[44] | Jonathan Aldrich. Resource-based programming in Plaid. Fun Ideas and Thoughts, June 2010. [ bib | .pdf ] |
[45] | Jonathan Aldrich. The power of interoperability: why objects are inevitable. In ACM Symposium on New Ideas in Programming and Reflections on Software (Onward!), pages 101--116, October 2013. [ bib | .pdf ] |
[46] | Jonathan Aldrich, Ronald Garcia, Mark Hahnenberg, Manuel Mohr, Karl Naden, Darpan Saini, Sven Stork, Joshua Sunshine, Éric Tanter, and Roger Wolff. Permission-based programming languages. In International Conference on Software Engineering (ICSE), pages 828--831, May 2011. [ bib | .pdf ] |
[47] | Jonathan Aldrich, Joshua Sunshine, Darpan Saini, and Zachary Sparks. Typestate-oriented programming. In Companion to Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 1015--1022, October 2009. [ bib | .pdf ] |
[48] | Guillaume Allais, James Chapman, Conor McBride, and James McKinna. Type-and-scope safe programs and their proofs. In Certified Programs and Proofs (CPP), pages 195--207, January 2017. [ bib | .pdf ] |
[49] | Paulo Sérgio Almeida. Balloon types: Controlling sharing of state in data types. In European Conference on Object-Oriented Programming (ECOOP), volume 1241 of Lecture Notes in Computer Science, pages 32--59. Springer, June 1997. [ bib | http ] |
[50] | Stephen Alstrup, Mikkel Thorup, Inge Li Gørtz, Theis Rauhe, and Uri Zwick. Union-find with constant time deletions. ACM Transactions on Algorithms, 11(1):6:1--6:28, 2014. [ bib | http ] |
[51] | Thorsten Altenkirch, Nils Anders Danielsson, Andres Löh, and Nicolas Oury. ΠΣ: Dependent types without the sugar. In Functional and Logic Programming, volume 6009 of Lecture Notes in Computer Science, pages 40--55. Springer, April 2010. [ bib | .pdf ] |
[52] | Thorsten Altenkirch, Conor McBride, and James McKinna. Why dependent types matter. Unpublished, April 2005. [ bib | .pdf ] |
[53] | Thorsten Altenkirch and Bernhard Reus. Monadic presentations of lambda terms using generalized inductive types. In Computer Science Logic, volume 1683 of Lecture Notes in Computer Science, pages 453--468. Springer, 1999. [ bib | .pdf ] |
[54] | Roberto Amadio and Yann Régis-Gianas. Certifying and reasoning on cost annotations of functional programs. In Foundational and Practical Aspects of Resource Analysis, volume 7177 of Lecture Notes in Computer Science, pages 72--89. Springer, May 2011. [ bib | http ] |
[55] | Roberto Amadio and Yann Régis-Gianas. Certifying and reasoning about cost annotations of functional programs. Higher-Order and Symbolic Computation, January 2013. [ bib | http ] |
[56] | Roberto M. Amadio, Nicholas Ayache, François Bobot, Jaap Boender, Brian Campbell, Ilias Garnier, Antoine Madet, James McKinna, Dominic P. Mulligan, Mauro Piccolo, Randy Pollack, Yann Régis-Gianas, Claudio Sacerdoti Coen, Ian Stark, and Paolo Tranquilli. Certified complexity (CerCo). In Foundational and Practical Aspects of Resource Analysis, volume 8552 of Lecture Notes in Computer Science, pages 1--18. Springer, August 2014. [ bib | http ] |
[57] | Roberto M. Amadio and Luca Cardelli. Subtyping recursive types. ACM Transactions on Programming Languages and Systems, 15(4):575--631, September 1993. [ bib | .pdf ] |
[58] | Pierre America and Jan Rutten. Solving reflexive domain equations in a category of complete metric spaces. In Mathematical Foundations of Programming Semantics, volume 298 of Lecture Notes in Computer Science, pages 254--288. Springer, 1988. [ bib | http ] |
[59] | Afshin Amighi, Christian Haack, Marieke Huisman, and Clément Hurlin. Permission-based separation logic for multithreaded Java programs. Logical Methods in Computer Science, 11(1):1--66, 2015. [ bib | http ] |
[60] | Nada Amin, Samuel Grütter, Martin Odersky, Tiark Rompf, and Sandro Stucki. The essence of dependent object types. In A List of Successes That Can Change the World -- Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, volume 9600 of Lecture Notes in Computer Science, pages 249--272. Springer, 2016. [ bib | .pdf ] |
[61] | Nada Amin and Tiark Rompf. Type soundness proofs with definitional interpreters. In Principles of Programming Languages (POPL), pages 666--679, January 2017. [ bib | .pdf ] |
[62] | Henrik Reif Andersen. Model checking and Boolean graphs. Theoretical Computer Science, 126(1):3--30, 1994. [ bib | http ] |
[63] | Brian Anderson, Lars Bergstrom, David Herman, Josh Matthews, Keegan McAllister, Manish Goregaokar, Jack Moffitt, and Simon Sapin. Experience report: Developing the Servo web browser engine using Rust. 2015. [ bib | http ] |
[64] | T. Anderson, J. Eve, and J. J. Horning. Efficient LR(1) parsers. Acta Informatica, 2:12--39, 1973. [ bib | http ] |
[65] | Gregory R. Andrews. Foundations of multithreaded, parallel, and distributed programming. Addison-Wesley, 2000. [ bib ] |
[66] | 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 ] |
[67] | Peter B. Andrews. An introduction to mathematical logic and type theory: to truth through proof. Academic Press, 1986. [ bib ] |
[68] | Timos Antonopoulos, Nikos Gorogiannis, Christoph Haase, Max I. Kanovich, and Joël Ouaknine. Foundations for decision problems in separation logic with general inductive predicates. In Foundations of Software Science and Computation Structures (FOSSACS), volume 8412 of Lecture Notes in Computer Science, pages 411--425. Springer, April 2014. [ bib | .pdf ] |
[69] | 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, September 1996. [ bib | http ] |
[70] | Andrew Appel. Modern compiler implementation in ML. Cambridge University Press, 1998. [ bib | http ] |
[71] | Andrew W. Appel. Compiling with continuations. Cambridge University Press, 1992. [ bib | http ] |
[72] | Andrew W. Appel. Verified software toolchain. In European Symposium on Programming (ESOP), volume 6602 of Lecture Notes in Computer Science, pages 1--17. Springer, March 2011. [ bib | .pdf ] |
[73] | Andrew W. Appel. VeriSmall: Verified Smallfoot shape analysis. In Certified Programs and Proofs (CPP), volume 7086 of Lecture Notes in Computer Science, pages 231--246. Springer, December 2011. [ bib | .pdf ] |
[74] | Andrew W. Appel and Trevor Jim. Shrinking lambda expressions in linear time. Journal of Functional Programming, 7(5):515--540, 1997. [ bib | .ps.gz ] |
[75] | Andrew W. Appel, Paul-André Melliès, Christopher D. Richards, and Jérôme Vouillon. A very modal model of a modern, major, general type system. In Principles of Programming Languages (POPL), pages 109--122, January 2007. [ bib | .pdf ] |
[76] | 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 ] |
[77] | Zena M. Ariola and Jan Willem Klop. Equational term graph rewriting. Fundamenta Informaticæ, 26(3--4):207--240, 1996. [ bib | .ps.Z ] |
[78] | André Arnold and Paul Crubillé. A linear algorithm to solve fixed-point equations on transition systems. Information Processing Letters, 29(2):57--66, 1988. [ bib | http ] |
[79] | André Arnold and Maurice Nivat. The metric space of infinite trees. Algebraic and topological properties. Fundamenta Informaticæ, 3(4):181--205, 1980. [ bib ] |
[80] | Kenichi Asai and Yukiyoshi Kameyama. Polymorphic delimited continuations. In Asian Symposium on Programming Languages and Systems (APLAS), volume 4807 of Lecture Notes in Computer Science, pages 239--254. Springer, November 2007. [ bib | .pdf ] |
[81] | David Aspinall, Lennart Beringer, Martin Hofmann, Hans-Wolfgang Loidl, and Alberto Momigliano. A program logic for resources. Theoretical Computer Science, 389(3):411--445, 2007. [ bib | .pdf ] |
[82] | David Aspinall and Martin Hofmann. Another type system for in-place update. In European Symposium on Programming (ESOP), volume 2305 of Lecture Notes in Computer Science, pages 36--52. Springer, April 2002. [ bib | .pdf ] |
[83] | David Aspinall, Martin Hofmann, and Michal Konečný. A type system with usage aspects. Journal of Functional Programming, 18(2):141--178, 2008. [ bib | http ] |
[84] | Robert Atkey. Parameterised notions of computation. Journal of Functional Programming, 19(3--4):355--376, 2009. [ bib | .pdf ] |
[85] | Robert Atkey. Syntax for free: representing syntax with binding using parametricity. In Typed Lambda Calculi and Applications (TLCA), volume 5608 of Lecture Notes in Computer Science, pages 35--49. Springer, July 2009. [ bib | .pdf ] |
[86] | Robert Atkey. Amortised resource analysis with separation logic. In European Symposium on Programming (ESOP), volume 6012 of Lecture Notes in Computer Science, pages 85--103. Springer, 2010. [ bib | .pdf ] |
[87] | Robert Atkey. Amortised resource analysis with separation logic. Logical Methods in Computer Science, 7(2:17), 2011. [ bib | .pdf ] |
[88] | Robert Atkey, Sam Lindley, and Jeremy Yallop. Unembedding domain-specific languages. In Haskell symposium, pages 37--48, September 2009. [ bib | .pdf ] |
[89] | Lennart Augustsson. Implementing Haskell overloading. In Functional Programming Languages and Computer Architecture (FPCA), pages 65--73, 1993. [ bib | http ] |
[90] | Jean-Michel Autebert. Théorie des langages et des automates. Masson, 1994. [ bib ] |
[91] | 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, 1997. [ bib | .ps.gz ] |
[92] | Jeremy Avigad and Kevin Donnelly. Formalizing O notation in Isabelle/HOL. In International Joint Conference on Automated Reasoning, volume 3097 of Lecture Notes in Computer Science, pages 357--371. Springer, July 2004. [ bib | .pdf ] |
[93] | Nicholas Ayache, Roberto M. Amadio, and Yann Régis-Gianas. Certifying and reasoning on cost annotations in C programs. In Formal Methods for Industrial Critical Systems, volume 7437 of Lecture Notes in Computer Science, pages 32--46. Springer, August 2012. [ bib | http ] |
[94] | John Aycock and Nigel Horspool. Simple generation of static single-assignment form. In Compiler Construction (CC), volume 1781 of Lecture Notes in Computer Science. Springer, March 2000. [ bib | .ps ] |
[95] | Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, and Stephanie Weirich. Engineering formal metatheory. In Principles of Programming Languages (POPL), pages 3--15, January 2008. [ bib | .pdf ] |
[96] | Brian Aydemir and Stephanie Weirich. LNgen: Tool support for locally nameless representations. Technical Report MS-CIS-10-24, University of Pennsylvania Department of Computer and Information Science, June 2010. [ bib | http ] |
[97] | 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 Theorem Proving in Higher Order Logics (TPHOLs), volume 3603 of Lecture Notes in Computer Science, pages 50--65. Springer, August 2005. [ bib | .pdf ] |
[98] | Henry G. Baker. List processing in real time on a serial computer. Communications of the ACM, 21(4):280--294, April 1978. [ bib | http ] |
[99] | 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 ] |
[100] | Thibaut Balabonski, François Pottier, and Jonathan Protzenko. Type soundness and race freedom for Mezzo. In Proceedings of the 12th International Symposium on Functional and Logic Programming (FLOPS 2014), volume 8475 of Lecture Notes in Computer Science, pages 253--269. Springer, June 2014. [ bib | .pdf ] |
[101] | Thibaut Balabonski, François Pottier, and Jonathan Protzenko. The design and formalization of Mezzo, a permission-based programming language. ACM Transactions on Programming Languages and Systems, 38(4):14:1--14:94, August 2016. [ bib | .pdf ] |
[102] | Vincent Balat, Roberto Di Cosmo, and Marcelo Fiore. Remarks on isomorphisms in typed lambda calculi with empty and sum type. In Logic in Computer Science (LICS), July 2002. [ bib | .ps.gz ] |
[103] | Anindya Banerjee, Nevin Heintze, and Jon G. Riecke. Region analysis and the polymorphic lambda calculus. In Logic in Computer Science (LICS), pages 88--97, July 1999. [ bib | .pdf ] |
[104] | 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, October 2001. [ bib | .ps.gz ] |
[105] | 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 ] |
[106] | 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 ] |
[107] | Anindya Banerjee and David A. Naumann. Representation independence, confinement, and access control. In Principles of Programming Languages (POPL), pages 166--177, January 2002. [ bib | .ps ] |
[108] | Anindya Banerjee and David A. Naumann. State based ownership, reentrance, and encapsulation. In European Conference on Object-Oriented Programming (ECOOP), volume 3586 of Lecture Notes in Computer Science, pages 387--411. Springer, July 2005. [ bib | .pdf ] |
[109] | 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, 1994. [ bib | .ps.Z ] |
[110] | Andrew Barber. Dual intuitionistic linear logic. Technical Report ECS-LFCS-96-347, Laboratory for Foundations of Computer Science, School of Informatics at the University of Edinburgh, September 1996. [ bib | http ] |
[111] | Henk P. Barendregt. The lambda calculus, its syntax and semantics. Elsevier Science, 1984. [ bib | http ] |
[112] | 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 ] |
[113] | 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, 1995. [ bib | http ] |
[114] | Mike Barnett, Bor-Yuh Evan Chang, Rob DeLine, Bart, and Jacobs. Boogie: A modular reusable verifier for object-oriented programs. In Formal Methods for Components and Objects. Springer, November 2005. [ bib | .pdf ] |
[115] | Mike Barnett, Rob DeLine, Manuel Fähndrich, K. Rustan M. Leino, and Wolfram Schulte. Verification of object-oriented programs with invariants. Journal of Object Technology, 3(6), 2004. [ bib | http ] |
[116] | Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte. The Spec# programming system: An overview. In Construction and Analysis of Safe, Secure and Interoperable Smart devices (CASSIS), volume 3362 of Lecture Notes in Computer Science, pages 49--69. Springer, 2004. [ bib | .pdf ] |
[117] | 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 ] |
[118] | Chris Barrett, Riko Jacob, and Madhav Marathe. Formal language constrained path problems. SIAM Journal on Computing, 30(3):809--837, 2000. [ bib | .ps.gz ] |
[119] | 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 ] |
[120] | Gilles Barthe, Julien Forest, David Pichardie, and Vlad Rusu. Defining and reasoning about recursive functions: A practical tool for the Coq proof assistant. In Functional and Logic Programming, volume 3945 of Lecture Notes in Computer Science, pages 114--129. Springer, April 2006. [ bib | .pdf ] |
[121] | Gilles Barthe, John Hatcliff, and Morten Heine Sørensen. CPS translations and applications: The cube and beyond. Higher-Order and Symbolic Computation, 12(2):125--170, 1999. [ bib | http ] |
[122] | Aditi Barthwal and Michael Norrish. Verified, executable parsing. In European Symposium on Programming (ESOP), volume 5502 of Lecture Notes in Computer Science, pages 160--174. Springer, 2009. [ bib | .pdf ] |
[123] | 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 ] |
[124] | Andrej Bauer, Martin Hofmann, and Aleksandr Karbyshev. On monadic parametricity of second-order functionals. In Foundations of Software Science and Computation Structures (FOSSACS), volume 7794 of Lecture Notes in Computer Science, pages 225--240. Springer, March 2013. [ bib | .pdf ] |
[125] | Andrej Bauer and Matija Pretnar. An effect system for algebraic effects and handlers. Logical Methods in Computer Science, 10(4), 2014. [ bib | .pdf ] |
[126] | 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 ] |
[127] | C. J. Bell, Robert Dockins, Aquinas Hobor, Andrew W. Appel, and David Walker. Comparing semantic and syntactic methods in mechanized proof frameworks. In International Workshop on Proof-Carrying Code (PCC), June 2008. [ bib | .pdf ] |
[128] | 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 ] |
[129] | Jeffrey M. Bell, Françoise Bellegarde, and James Hook. Type-driven defunctionalization. In International Conference on Functional Programming (ICFP), August 1997. [ bib | http ] |
[130] | Michael A. Bender, Jeremy T. Fineman, Seth Gilbert, and Robert E. Tarjan. A new approach to incremental cycle detection and related problems. ACM Transactions on Algorithms, 12(2):14:1--14:22, 2016. [ bib | http ] |
[131] | Jesper Bengtson, Jonas Braband Jensen, and Lars Birkedal. Charge! A framework for higher-order separation logic in Coq. In Interactive Theorem Proving (ITP), pages 315--331, August 2012. [ bib | .pdf ] |
[132] | Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn. A decidable fragment of separation logic. In Foundations of Software Technology and Theoretical Computer Science (FSTTCS), volume 3328 of Lecture Notes in Computer Science, pages 97--109. Springer, December 2004. [ bib | .pdf ] |
[133] | Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn. Smallfoot: Modular automatic assertion checking with separation logic. In Formal Methods for Components and Objects, volume 4111 of Lecture Notes in Computer Science, pages 115--137. Springer, November 2005. [ bib | .pdf ] |
[134] | 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, 2005. [ bib | .pdf ] |
[135] | 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 ] |
[136] | Josh Berdine, Peter W. O'Hearn, Uday S. Reddy, and Hayo Thielecke. Linear continuation-passing. Higher-Order and Symbolic Computation, 15(2--3):181--208, 2002. [ bib | .pdf ] |
[137] | Martin Berger, Kohei Honda, and Nobuko Yoshida. A logical analysis of aliasing in imperative higher-order functions. In International Conference on Functional Programming (ICFP), pages 280--293, September 2005. [ bib | http ] |
[138] | K. Bernstein and E. W. Stark. Debugging type errors. Unpublished, November 1995. [ bib | .ps.gz ] |
[139] | 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 ] |
[140] | Yves Bertot and Pierre Castéran. Interactive theorem proving and program development -- Coq'Art: The calculus of inductive constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004. [ bib | .pdf ] |
[141] | Frédéric Besson, Thomas de Grenier de Latour, and Thomas Jensen. Secure calling contexts for stack inspection. In Principles and Practice of Declarative Programming (PPDP), pages 76--87, October 2002. [ bib | .pdf ] |
[142] | 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 ] |
[143] | Achyutram Bhamidipaty and Todd A. Proebsting. Very fast YACC-compatible parsers (for very little effort). Software: Practice and Experience, 28(2):181--190, February 1998. [ bib | .ps ] |
[144] | Karthik Bhargavan, Cédric Fournet, and Andy Gordon. Modular verification of security protocol code by typing. In Principles of Programming Languages (POPL), pages 445--456, January 2010. [ bib | .pdf ] |
[145] | Karthik Bhargavan, Cédric Fournet, Andy Gordon, Sergio Maffeis, and Jesper Bengtson. The F7 typechecker, 2011. http://research.microsoft.com/en-us/projects/f7/. [ bib | http ] |
[146] | Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, and Pierre-Yves Strub. Implementing TLS with verified cryptographic security. In IEEE Symposium on Security and Privacy (S&P), pages 445--459, May 2013. [ bib | .pdf ] |
[147] | Girish Bhat and Rance Cleaveland. Efficient local model-checking for fragments of the modal μ-calculus. In Tools and Algorithms for Construction and Analysis of Systems (TACAS), volume 1055 of Lecture Notes in Computer Science, pages 107--126. Springer, March 1996. [ bib | .ps.gz ] |
[148] | Armin Biere, Alessandro Cimatti, Edmund Clarke, and Yunshan Zhu. Symbolic model checking without BDDs. In Tools and Algorithms for Construction and Analysis of Systems (TACAS), volume 1579 of Lecture Notes in Computer Science, pages 193--207. Springer, March 1999. [ bib | .pdf ] |
[149] | Kevin Bierhoff and Jonathan Aldrich. Modular typestate checking of aliased objects. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 301--320, October 2007. [ bib | .pdf ] |
[150] | Kevin Bierhoff, Nels E. Beckman, and Jonathan Aldrich. Practical API protocol checking with access permissions. In European Conference on Object-Oriented Programming (ECOOP), volume 5653 of Lecture Notes in Computer Science, pages 195--219. Springer, July 2009. [ bib | .pdf ] |
[151] | Kevin Bierhoff, Nels E. Beckman, and Jonathan Aldrich. Checking concurrent typestate with access permissions in Plural: A retrospective. In Peri L. Tarr and Alexander L. Wolf, editors, Engineering of Software, pages 35--48. Springer, 2011. [ bib | .pdf ] |
[152] | 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, April 2005. [ bib | .pdf ] |
[153] | Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski. Abstracting algebraic effects. Proceedings of the ACM on Programming Languages, 3(POPL):6:1--6:28, 2019. [ bib | .pdf ] |
[154] | Richard Bird and Lambert Meertens. Nested datatypes. In Mathematics of Program Construction (MPC), volume 1422 of Lecture Notes in Computer Science, pages 52--67. Springer, 1998. [ bib | .pdf ] |
[155] | Richard Bird and Ross Paterson. de Bruijn notation as a nested datatype. Journal of Functional Programming, 9(1):77--91, January 1999. [ bib | http ] |
[156] | Richard S. Bird and John Hughes. The alpha-beta algorithm: An exercise in program transformation. Information Processing Letters, 24(1):53--57, 1987. [ bib | http ] |
[157] | Lars Birkedal, Bernhard Reus, Jan Schwinghammer, Kristian Støvring, Jacob Thamsborg, and Hongseok Yang. Step-indexed Kripke models over recursive worlds. In Principles of Programming Languages (POPL), pages 119--132, January 2011. [ bib | .pdf ] |
[158] | 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 ] |
[159] | Lars Birkedal, Jan Schwinghammer, and Kristian Støvring. A metric model of lambda calculus with guarded recursion. Presented at FICS 2010, July 2010. [ bib | .pdf ] |
[160] | Lars Birkedal, Kristian Støvring, and Jacob Thamsborg. The category-theoretic solution of recursive metric-space quations. Technical Report ITU-2009-119, IT University of Copenhagen, 2009. [ bib | .pdf ] |
[161] | Lars Birkedal, Kristian Støvring, and Jacob Thamsborg. Realizability semantics of parametric polymorphism, general references, and recursive types. In Foundations of Software Science and Computation Structures (FOSSACS), volume 5504 of Lecture Notes in Computer Science, pages 456--470. Springer, March 2009. [ bib | .pdf ] |
[162] | Lars Birkedal, Kristian Støvring, and Jacob Thamsborg. Realisability semantics of parametric polymorphism, general references, and recursive types. Mathematical Structures in Computer Science, 20(4):655--703, 2010. [ bib | .pdf ] |
[163] | Lars Birkedal and Mads Tofte. A constraint-based region inference algorithm. Theoretical Computer Science, 258:299--392, 2001. [ bib | .ps.gz ] |
[164] | 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 ] |
[165] | Andrew D. Birrell. An introduction to programming with C# threads. Manuscript, 2003. [ bib | .pdf ] |
[166] | Sandip K. Biswas. Dynamic slicing in higher-order programming languages. PhD thesis, University of Pennsylvania, August 1997. [ bib ] |
[167] | Régis Blanc, Viktor Kuncak, Etienne Kneuss, and Philippe Suter. An overview of the Leon verification system: verification by translation to recursive functions. In Workshop on Scala, pages 1:1--1:10, July 2013. [ bib | .pdf ] |
[168] | Frédéric Blanqui and Adam Koprowski. CoLoR: a coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. Mathematical Structures in Computer Science, 21(4):827--859, August 2011. [ bib | .pdf ] |
[169] | Guy E. Blelloch and John Greiner. Parallelism in sequential functional languages. In Functional Programming Languages and Computer Architecture (FPCA), pages 226--237, 1995. [ bib | .ps.gz ] |
[170] | François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. Let's verify this with Why3. Software Tools for Technology Transfer, 17(6):709--727, 2015. [ bib | http ] |
[171] | Robert L. Bocchino Jr. Alias control for deterministic parallelism. In Dave Clarke, James Noble, and Tobias Wrigstad, editors, Aliasing in Object-Oriented Programming. Types, Analysis and Verification, volume 7850 of Lecture Notes in Computer Science, pages 156--195. Springer, 2013. [ bib | http ] |
[172] | Robert L. Bocchino Jr. and Vikram S. Adve. Types, regions, and effects for safe programming with object-oriented parallel frameworks. In European Conference on Object-Oriented Programming (ECOOP), volume 6813 of Lecture Notes in Computer Science, pages 306--332. Springer, July 2011. [ bib | .pdf ] |
[173] | Robert L. Bocchino Jr., Vikram S. Adve, Sarita V. Adve, and Marc Snir. Parallel programming must be deterministic by default. In USENIX Conference on Hot Topics in Parallelism (HotPar), pages 1--6, 2009. [ bib | .pdf ] |
[174] | Robert L. Bocchino Jr., Vikram S. Adve, Danny Dig, Sarita V. Adve, Stephen Heumann, Rakesh Komuravelli, Jeffrey Overbey, Patrick Simmons, Hyojin Sung, and Mohsen Vakilian. A type and effect system for deterministic parallel Java. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 97--116, October 2009. [ bib | .pdf ] |
[175] | Robert L. Bocchino Jr., Stephen Heumann, Nima Honarmand, Sarita V. Adve, Vikram S. Adve, Adam Welc, and Tatiana Shpeisman. Safe nondeterminism in a deterministic-by-default parallel language. In Principles of Programming Languages (POPL), pages 535--548, January 2011. [ bib | .pdf ] |
[176] | Chiara Bodei, Pierpaolo Degano, Flemming Nielson, and Hanne Riis Nielson. Static analysis of processes for no read-up and no write-down. In Foundations of Software Science and Computation Structures (FOSSACS), volume 1578 of Lecture Notes in Computer Science, pages 120--134. Springer, March 1999. [ bib | .ps ] |
[177] | Hans-J. Boehm and Sarita V. Adve. You don't know jack about shared variables or memory models. Communications of the ACM, 55(2):48--54, February 2012. [ bib | http ] |
[178] | Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Wave equation numerical resolution: a comprehensive mechanized proof of a C program. Journal of Automated Reasoning, 50(4):423--456, April 2013. [ bib | http ] |
[179] | Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Coquelicot: A user-friendly library of real analysis for Coq. Mathematics in Computer Science, 9(1):41--62, March 2015. [ bib | http ] |
[180] | Daniel Bonniot. Type-checking multi-methods in ML (a modular approach). In Foundations of Object-Oriented Languages (FOOL), January 2002. [ bib | .ps ] |
[181] | Urban Boquist. Code optimisation techniques for lazy functional languages. PhD thesis, Chalmers University of Technology, April 1999. [ bib | .pdf ] |
[182] | Michele Boreale and Davide Sangiorgi. A fully abstract semantics for causality in the π-calculus. Acta Informatica, 35(5):353--400, May 1998. [ bib | .pdf ] |
[183] | Johannes Borgström, Juan Chen, , and Nikhil Swamy. Verified stateful programs with substructural state and Hoare types. In Programming Languages Meets Program Verification (PLPV), January 2011. [ bib | .pdf ] |
[184] | Richard Bornat. Proving pointer programs in Hoare logic. In Mathematics of Program Construction (MPC), volume 1837 of Lecture Notes in Computer Science, pages 102--126. Springer, 2000. [ bib | .pdf ] |
[185] | Richard Bornat, Cristiano Calcagno, Peter O'Hearn, and Matthew Parkinson. Permission accounting in separation logic. In Principles of Programming Languages (POPL), pages 259--270, January 2005. [ bib | .pdf ] |
[186] | Ahmed Bouajjani, Javier Esparza, and Oded Maler. Reachability analysis of pushdown automata: Application to model-checking. In International Conference on Concurrency Theory (CONCUR), volume 1243 of Lecture Notes in Computer Science, pages 135--150. Springer, July 1997. [ bib | .pdf ] |
[187] | Gérard Boudol. Typing termination in a higher-order concurrent imperative language. Information and Computation, 2009. To appear. [ bib | .pdf ] |
[188] | Gérard Boudol and Ilaria Castellani. Non-interference for concurrent programs and thread systems. To appear, September 2001. [ bib | .ps.gz ] |
[189] | Sylvain Boulmé. Intuitionistic refinement calculus. In Typed Lambda Calculi and Applications (TLCA), volume 4583 of Lecture Notes in Computer Science, pages 54--69. Springer, June 2007. [ bib | .pdf ] |
[190] | 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 ] |
[191] | François Bourdoncle and Stephan Merz. Type checking higher-order polymorphic multi-methods. In Principles of Programming Languages (POPL), pages 302--315, January 1997. [ bib | .html ] |
[192] | Chandrasekhar Boyapati, Robert Lee, and Martin Rinard. Ownership types for safe programming: preventing data races and deadlocks. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 211--230, November 2002. [ bib | http ] |
[193] | Chandrasekhar Boyapati, Barbara Liskov, and Liuba Shrira. Ownership types for object encapsulation. In Principles of Programming Languages (POPL), pages 213--223, January 2003. [ bib | .pdf ] |
[194] | John Boyland. Alias burying: Unique variables without destructive reads. Science of Computer Programming, 31(6):533--553, May 2001. [ bib | .ps ] |
[195] | John Boyland. Checking interference with fractional permissions. In Static Analysis Symposium (SAS), volume 2694 of Lecture Notes in Computer Science, pages 55--72. Springer, June 2003. [ bib | .pdf ] |
[196] | John Boyland, James Noble, and William Retert. Capabilities for sharing: A generalisation of uniqueness and read-only. In European Conference on Object-Oriented Programming (ECOOP), volume 2072 of Lecture Notes in Computer Science, pages 2--27. Springer, June 2001. [ bib | .ps ] |
[197] | John Tang Boyland. Semantics of fractional permissions with nesting. ACM Transactions on Programming Languages and Systems, 32(6):22:1--22:33, 2010. [ bib | http ] |
[198] | John Tang Boyland and William Retert. Connecting effects and uniqueness with adoption. In Principles of Programming Languages (POPL), pages 283--295, January 2005. [ bib | .pdf ] |
[199] | Gilad Bracha and William Cook. Mixin-based inheritance. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 303--311, 1990. [ bib | .ps ] |
[200] | Gilad Bracha and Gary Lindstrom. Modularity meets inheritance. Technical Report UUCS-91-017, University of Utah, October 1991. [ bib | .ps ] |
[201] | Aaron R. Bradley and Zohar Manna. The calculus of computation. Springer, 2007. [ bib | http ] |
[202] | Thomas Braibant and Damien Pous. Tactics for reasoning modulo AC in Coq. In Certified Programs and Proofs (CPP), volume 7086 of Lecture Notes in Computer Science, pages 167--182. Springer, 2011. [ bib | http ] |
[203] | 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 ] |
[204] | Michael Brandt and Fritz Henglein. Coinductive axiomatization of recursive type equality and subtyping. Fundamenta Informaticæ, 33:309--338, 1998. [ bib | .ps.gz ] |
[205] | Gilles Brassard and Paul Bratley. Fundamentals of algorithmics. Prentice Hall, 1996. [ bib ] |
[206] | 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 ] |
[207] | Stephen Brookes and Peter W. O'Hearn. Concurrent separation logic. SIGLOG News, 3(3):47--65, 2016. [ bib | http ] |
[208] | Stephen D. Brookes. A semantics for concurrent separation logic. In International Conference on Concurrency Theory (CONCUR), volume 3170 of Lecture Notes in Computer Science, pages 16--34. Springer, August 2004. [ bib | http ] |
[209] | James Brotherston, Dino Distefano, and Rasmus Lerchedahl Petersen. Automated cyclic entailment proofs in separation logic. In International Conference on Automated Deduction (CADE), volume 6803 of Lecture Notes in Computer Science, pages 131--146. Springer, July 2011. [ bib | .pdf ] |
[210] | 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 ] |
[211] | Kim Bruce, Roberto Di Cosmo, and Giuseppe Longo. Provable isomorphisms of types. Mathematical Structures in Computer Science, 2(2):231--247, 1992. [ bib | .dvi ] |
[212] | Kim B. Bruce, Luca Cardelli, and Benjamin C. Pierce. Comparing object encodings. Information and Computation, 155(1/2):108--133, November 1999. [ bib | .ps ] |
[213] | Julian Brunner and Peter Lammich. Formal verification of an executable LTL model checker with partial order reduction. Journal of Automated Reasoning, 60(1):3--21, 2018. [ bib | .pdf ] |
[214] | Peter Buchlovsky and Hayo Thielecke. A type-theoretic reconstruction of the visitor pattern. Electronic Notes in Theoretical Computer Science, 155:309--329, 2006. [ bib | .pdf ] |
[215] | Michele Bugliesi, Stefano Calzavara, Fabienne Eigner, and Matteo Maffei. Affine refinement types for secure distributed programming. To appear, 2015. [ bib | .pdf ] |
[216] | Michele Bugliesi and Silvia Crafa. Object calculi for dynamic messages. In Foundations of Object-Oriented Languages (FOOL), 1999. [ bib ] |
[217] | 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 ] |
[218] | Alexandre Buisse, Lars Birkedal, and Kristian Støvring. A step-indexed Kripke model of separation logic for storable locks. Electronic Notes in Theoretical Computer Science, 276:121--143, September 2011. [ bib | .pdf ] |
[219] | Lukas Bulwahn, Alexander Krauss, Florian Haftmann, Levent Erkök, and John Matthews. Imperative functional programming with Isabelle/HOL. In Theorem Proving in Higher Order Logics (TPHOLs), volume 5170 of Lecture Notes in Computer Science, pages 134--149. Springer, August 2008. [ bib | .pdf ] |
[220] | Peter Buneman and Atsushi Ohori. Polymorphism and type inference in database programming. ACM Transactions on Database Systems, 21(1):30--76, 1996. [ bib | .pdf ] |
[221] | 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. Software Tools for Technology Transfer, 7(3):212--232, June 2005. [ bib | .pdf ] |
[222] | 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 ] |
[223] | Jiazhen Cai and Robert Paige. Program derivation by fixed point computation. Science of Computer Programming, 11(3):197--261, 1989. [ bib | .ps ] |
[224] | Luís Caires and João Costa Seco. The type discipline of behavioral separation. In Principles of Programming Languages (POPL), pages 275--286, January 2013. [ bib | http ] |
[225] | Cristiano Calcagno and Dino Distefano. Infer: An automatic program verifier for memory safety of C programs. In NASA Formal Methods (NFM), volume 6617 of Lecture Notes in Computer Science, pages 459--465. Springer, April 2011. [ bib | .pdf ] |
[226] | Cristiano Calcagno, Dino Distefano, Jérémy Dubreil, Dominik Gabi, Pieter Hooimeijer, Martino Luca, Peter W. O'Hearn, Irene Papakonstantinou, Jim Purbrick, and Dulma Rodriguez. Moving fast with software verification. In NASA Formal Methods (NFM), volume 9058 of Lecture Notes in Computer Science, pages 3--11. Springer, April 2015. [ bib | http ] |
[227] | Cristiano Calcagno, Dino Distefano, and Peter O'Hearn. Open-sourcing Facebook Infer: Identify bugs before you ship. https://code.facebook.com/posts/1648953042007882/open-sourcing-facebook-infer-identify-bugs-before-you-ship/, June 2015. [ bib ] |
[228] | Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, and Hongseok Yang. Compositional shape analysis by means of bi-abduction. In Principles of Programming Languages (POPL), pages 289--300, January 2009. [ bib | .pdf ] |
[229] | Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, and Hongseok Yang. Compositional shape analysis by means of bi-abduction. Journal of the ACM, 58(6), 2011. [ bib | .pdf ] |
[230] | Cristiano Calcagno, Dino Distefano, and Viktor Vafeiadis. Bi-abductive resource invariant synthesis. In Asian Symposium on Programming Languages and Systems (APLAS), volume 5904 of Lecture Notes in Computer Science, pages 259--274. Springer, December 2009. [ bib | .pdf ] |
[231] | 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 ] |
[232] | 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 ] |
[233] | 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, 2004. [ bib | .pdf ] |
[234] | Cristiano Calcagno, Peter W. O'Hearn, and Hongseok Yang. Local action and abstract separation logic. In Logic in Computer Science (LICS), pages 366--378, July 2007. [ bib | .pdf ] |
[235] | Cristiano Calcagno, Hongseok Yang, and Peter W. O'Hearn. Computability and complexity results for a spatial assertion language for data structures. In Asian Symposium on Programming Languages and Systems (APLAS), pages 289--300, December 2001. [ bib | .ps ] |
[236] | Quentin Carbonneaux, Jan Hoffmann, Tahina Ramananandro, and Zhong Shao. End-to-end verification of stack-space bounds for C programs. In Programming Language Design and Implementation (PLDI), pages 270--281, June 2014. [ bib | .pdf ] |
[237] | Quentin Carbonneaux, Jan Hoffmann, Thomas Reps, and Zhong Shao. Automated resource analysis with Coq proof objects. In Computer Aided Verification (CAV), volume 10427 of Lecture Notes in Computer Science, pages 64--85. Springer, July 2017. [ bib | .pdf ] |
[238] | Luca Cardelli. Basic polymorphic typechecking. Science of Computer Programming, 8(2):147--172, 1987. [ bib | .pdf ] |
[239] | Luca Cardelli. A semantics of multiple inheritance. Information and Computation, 76(2/3):138--164, February 1988. [ bib | .pdf ] |
[240] | Luca Cardelli. Typeful programming. In Formal Description of Programming Concepts, IFIP State of the Art Reports Series. Springer, February 1989. [ bib | .pdf ] |
[241] | Luca Cardelli. The Quest language and system, 1991. [ bib | .pdf ] |
[242] | Luca Cardelli. Type systems. In Allen B. Tucker, editor, The Computer Science and Engineering Handbook, pages 2208--2236. CRC Press, 1997. [ bib | .pdf ] |
[243] | Luca Cardelli and Giuseppe Longo. A semantic basis for Quest. Journal of Functional Programming, 1(4):417--458, October 1991. [ bib | .pdf ] |
[244] | 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 ] |
[245] | 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 ] |
[246] | Luca Cardelli and Peter Wegner. On understanding types, data abstraction, and polymorphism. ACM Computing Surveys, 17(4):471--522, December 1985. [ bib | .pdf ] |
[247] | Felice Cardone. A coinductive completeness proof for the equivalence of recursive types. Theoretical Computer Science, 275(1--2):575--587, 2002. [ bib | http ] |
[248] | Felice Cardone and Mario Coppo. Type inference with recursive types: syntax and semantics. Information and Computation, 92(1):48--80, 1991. [ bib | http ] |
[249] | Jacques Carette. Gaussian elimination: a case study in efficient genericity with MetaOCaml. Science of Computer Programming, 62(1):3--24, September 2005. [ bib | .pdf ] |
[250] | Jacques Carette, Oleg Kiselyov, and Chung chieh Shan. Finally tagless, partially evaluated. In Asian Symposium on Programming Languages and Systems (APLAS), volume 4807 of Lecture Notes in Computer Science, pages 222--238. Springer, November 2007. [ bib | .pdf ] |
[251] | 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, 2004. [ bib | .pdf ] |
[252] | 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 ] |
[253] | Robert Cartwright. Notes on object-oriented program design, January 2000. [ bib | http ] |
[254] | Giuseppe Castagna. F_{<=}^{&} : integrating parametric and “ad hoc” second order polymorphism. In International Workshop on Database Programming Languages, Workshops in Computing. Springer, September 1993. [ bib ] |
[255] | 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 ] |
[256] | Giuseppe Castagna and Alain Frisch. A gentle introduction to semantic subtyping. In Principles and Practice of Declarative Programming (PPDP), pages 198--199, July 2005. [ bib | .pdf ] |
[257] | Henry Cejtin, Matthew Fluet, Suresh Jagannathan, and Stephen Weeks. The MLton compiler, 2007. [ bib | http ] |
[258] | 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, March 2000. [ bib | http ] |
[259] | Manuel M. T. Chakravarty, Gabriele Keller, Simon L. Peyton Jones, and Simon Marlow. Associated types with class. In Principles of Programming Languages (POPL), pages 1--13, January 2005. [ bib | .pdf ] |
[260] | 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 ] |
[261] | Bor-Yuh Evan Chang and Xavier Rival. Relational inductive shape analysis. In Principles of Programming Languages (POPL), pages 247--260, January 2008. [ bib | .pdf ] |
[262] | Arthur Charguéraud. Program verification through characteristic formulae. In International Conference on Functional Programming (ICFP), pages 321--332, September 2010. [ bib | .pdf ] |
[263] | Arthur Charguéraud. Characteristic formulae for the verification of imperative programs. In International Conference on Functional Programming (ICFP), pages 418--430, September 2011. [ bib | .pdf ] |
[264] | Arthur Charguéraud. The locally nameless representation. Journal of Automated Reasoning, 49(3):363--408, 2012. [ bib | .pdf ] |
[265] | Arthur Charguéraud. Characteristic formulae for mechanized program verification. PhD thesis, Université Paris 7, December 2010. [ bib | .pdf ] |
[266] | Arthur Charguéraud. The optimal fixed point combinator. In Interactive Theorem Proving (ITP), volume 6172 of Lecture Notes in Computer Science, pages 195--210. Springer, July 2010. [ bib | .pdf ] |
[267] | Arthur Charguéraud. Characteristic formulae for the verification of imperative programs, 2013. Unpublished. http://www.chargueraud.org/research/2013/cf/cf.pdf. [ bib ] |
[268] | Arthur Charguéraud. The CFML tool and library. http://www.chargueraud.org/softs/cfml/, 2019. [ bib ] |
[269] | Arthur Charguéraud and François Pottier. Functional translation of a calculus of capabilities. In International Conference on Functional Programming (ICFP), pages 213--224, September 2008. [ bib | .pdf ] |
[270] | Arthur Charguéraud and François Pottier. Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation. In Interactive Theorem Proving (ITP), volume 9236 of Lecture Notes in Computer Science, pages 137--153. Springer, August 2015. [ bib | .pdf ] |
[271] | Arthur Charguéraud and François Pottier. Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits. Journal of Automated Reasoning, September 2017. [ bib | .pdf ] |
[272] | Chih-Ping Chen and Paul Hudak. Rolling your own mutable ADT---a connection between linear types and monads. In Principles of Programming Languages (POPL), pages 54--66, January 1997. [ bib | .ps ] |
[273] | Chiyan Chen, Rui Shi, and Hongwei Xi. A typeful approach to object-oriented programming with multiple inheritance. In Practical Aspects of Declarative Languages (PADL), volume 3057 of Lecture Notes in Computer Science. Springer, June 2004. [ bib | .pdf ] |
[274] | Chiyan Chen and Hongwei Xi. Implementing typeful program transformations. In ACM Workshop on Evaluation and Semantics-Based Program Manipulation (PEPM), pages 20--28, June 2003. [ bib | .pdf ] |
[275] | Chiyan Chen and Hongwei Xi. Meta-programming through typeful code representation. In International Conference on Functional Programming (ICFP), pages 275--286, August 2003. [ bib | .pdf ] |
[276] | Chiyan Chen and Hongwei Xi. Combining programming with theorem proving. In International Conference on Functional Programming (ICFP), pages 66--77, September 2005. [ bib | .pdf ] |
[277] | Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. Using Crash Hoare logic for certifying the FSCQ file system. In Symposium on Operating Systems Principles (SOSP), pages 18--37, October 2015. [ bib | .pdf ] |
[278] | Juan Chen and David Tarditi. A simple typed intermediate language for object-oriented languages. In Principles of Programming Languages (POPL), pages 38--49, January 2005. [ bib | .pdf ] |
[279] | Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, and Laurent Théry. Formal proofs of Tarjan's algorithm in Why3, Coq, and Isabelle. Manuscript, October 2018. [ bib | .pdf ] |
[280] | Ran Chen and Jean-Jacques Lévy. A semi-automatic proof of strong connectivity. In Verified Software: Theories, Tools and Experiments, volume 10712 of Lecture Notes in Computer Science, pages 49--65. Springer, July 2017. [ bib | .pdf ] |
[281] | James Cheney. Scrap your nameplate. In International Conference on Functional Programming (ICFP), pages 180--191, September 2005. [ bib | .pdf ] |
[282] | James Cheney and Ralf Hinze. A lightweight implementation of generics and dynamics. In Haskell workshop, 2002. [ bib | .pdf ] |
[283] | James Cheney and Ralf Hinze. First-class phantom types. Technical Report 1901, Cornell University, 2003. [ bib | http ] |
[284] | 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, September 2004. [ bib | .pdf ] |
[285] | Perry Cheng and Guy E. Blelloch. A parallel, real-time garbage collector. In Programming Language Design and Implementation (PLDI), pages 125--136, June 2001. [ bib | .pdf ] |
[286] | Wei-Ngan Chin and Siau-Cheng Khoo. Calculating sized types. Higher-Order and Symbolic Computation, 14(2--3):261--300, September 2001. [ bib | http ] |
[287] | Olaf Chitil. Compositional explanation of types and algorithmic debugging of type errors. In International Conference on Functional Programming (ICFP), pages 193--204, September 2001. [ bib | .ps.gz ] |
[288] | Adam Chlipala. A certified type-preserving compiler from lambda calculus to assembly language. In Programming Language Design and Implementation (PLDI), pages 54--65, June 2007. [ bib | .pdf ] |
[289] | Adam Chlipala. Parametric higher-order abstract syntax for mechanized semantics. In International Conference on Functional Programming (ICFP), pages 143--156, September 2008. [ bib | .pdf ] |
[290] | Adam Chlipala. The Bedrock structured programming system: combining generative metaprogramming and Hoare logic in an extensible program verifier. In International Conference on Functional Programming (ICFP), pages 391--402, September 2013. [ bib | .pdf ] |
[291] | Adam Chlipala. Certified programming and dependent types. MIT Press, November 2013. [ bib | http ] |
[292] | Adam Chlipala. From network interface to multithreaded web applications: A case study in modular program verification. In Principles of Programming Languages (POPL), pages 609--622, January 2015. [ bib | .pdf ] |
[293] | Adam Chlipala, Gregory Malecha, Greg Morrisett, Avraham Shinnar, and Ryan Wisnesky. Effective interactive proofs for higher-order imperative programs. In International Conference on Functional Programming (ICFP), pages 79--90, September 2009. [ bib | .pdf ] |
[294] | Venkatesh Choppella. Unification source-tracking with application to diagnosis of type inference. PhD thesis, Indiana University, August 2002. [ bib | http ] |
[295] | Jacek Chrzaszcz. Polymorphic subtyping without distributivity. In International Symposium on Mathematical Foundations of Computer Science, volume 1450 of Lecture Notes in Computer Science, pages 346--355. Springer, August 1998. [ bib | .ps.gz ] |
[296] | Dave Clarke and Sophia Drossopoulou. Ownership, encapsulation and the disjointness of type and effect. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 292--310, November 2002. [ bib | .ps ] |
[297] | Dave Clarke, Sophia Drossopoulou, and James Noble. Aliasing, confinement, and ownership in object-oriented programming. In Object-Oriented Technology. ECOOP 2003 Workshop Reader, volume 3013 of Lecture Notes in Computer Science, pages 197--207. Springer, 2004. [ bib | http ] |
[298] | Dave Clarke, Johan Östlund, Ilya Sergey, and Tobias Wrigstad. Ownership types: A survey. In Aliasing in Object-Oriented Programming. Types, Analysis and Verification, volume 7850 of Lecture Notes in Computer Science, pages 15--58. Springer, 2013. [ bib | http ] |
[299] | Dave Clarke and Tobias Wrigstad. External uniqueness is unique enough. In European Conference on Object-Oriented Programming (ECOOP), volume 2743 of Lecture Notes in Computer Science, pages 176--200. Springer, July 2003. [ bib | .pdf ] |
[300] | David G. Clarke, James Noble, and John Potter. Simple ownership types for object containment. In European Conference on Object-Oriented Programming (ECOOP), volume 2072 of Lecture Notes in Computer Science, pages 53--76. Springer, June 2001. [ bib | .pdf ] |
[301] | David G. Clarke, John M. Potter, and James Noble. Ownership types for flexible alias protection. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 48--64, October 1998. [ bib | http ] |
[302] | 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 ] |
[303] | Rance Cleaveland and Bernhard Steffen. A linear-time model-checking algorithm for the alternation-free modal mu-calculus. In Computer Aided Verification (CAV), volume 575 of Lecture Notes in Computer Science, pages 48--58. Springer, 1991. [ bib | http ] |
[304] | 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 ] |
[305] | 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, April 2003. [ bib | .ps.gz ] |
[306] | Martin Clochard, Jean-Christophe Filliâtre, and Andrei Paskevich. How to avoid proving the absence of integer overflows. In Verified Software: Theories, Tools and Experiments, volume 9593 of Lecture Notes in Computer Science, pages 94--109. Springer, July 2015. [ bib | http ] |
[307] | Martin Clochard, Claude Marché, and Andrei Paskevich. Verified programs with binders. In Programming Languages Meets Program Verification (PLPV), pages 29--40, January 2014. [ bib | http ] |
[308] | Michael J. Coblenz, Joshua Sunshine, Jonathan Aldrich, Brad A. Myers, Sam Weber, and Forrest Shull. Exploring language support for immutability. In International Conference on Software Engineering (ICSE), pages 736--747, May 2016. [ bib | .pdf ] |
[309] | Albert Cohen, Sébastien Donadio, Maria-Jesus Garzaran, Christoph Herrmann, Oleg Kiselyov, and David Padua. In search of a program generator to implement generic transformations for high-performance computing. Science of Computer Programming, 62(1):25--46, September 2006. [ bib | .ps.gz ] |
[310] | Ernie Cohen, Markus Dahlweid, Mark A. Hillebrand, Dirk Leinenbach, Michal Moskal, Thomas Santen, Wolfram Schulte, and Stephan Tobies. VCC: A practical system for verifying concurrent C. In Theorem Proving in Higher Order Logics (TPHOLs), volume 5674 of Lecture Notes in Computer Science, pages 23--42. Springer, 2009. [ bib | http ] |
[311] | Dario Colazzo and Giorgio Ghelli. Subtyping recursive types in Kernel Fun. In Logic in Computer Science (LICS), pages 137--146, July 1999. [ bib ] |
[312] | Gregory D. Collins and Zhong Shao. Intensional analysis of higher-kinded recursive types. Technical Report YALEU/DCS/TR-1240, Yale University, 2002. [ bib | .pdf ] |
[313] | 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 ] |
[314] | Hubert Comon. Constraints in term algebras (short survey). In International Conference on Algebraic Methodology and Software Technology (AMAST), Workshops in Computing. Springer, 1993. [ bib | .ps ] |
[315] | Hubert Comon and Pierre Lescanne. Equational problems and disunification. Journal of Symbolic Computation, 7:371--425, 1989. [ bib | .pdf ] |
[316] | Sylvain Conchon and Evelyne Contejean. The Alt-Ergo automatic theorem prover, 2011. http://alt-ergo.lri.fr/. [ bib | http ] |
[317] | 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 ] |
[318] | Sylvain Conchon and Jean-Christophe Filliâtre. A persistent union-find data structure. In ACM Workshop on ML, pages 37--46, October 2007. [ bib | http ] |
[319] | Sylvain Conchon, Johannes Kanig, and Stéphane Lescuyer. Sat-Micro: petit mais costaud! In Journées Françaises des Langages Applicatifs (JFLA), January 2008. [ bib | .ps ] |
[320] | 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, April 2001. [ bib | .ps.gz ] |
[321] | Jeffrey Considine. Efficient hash-consing of recursive types. Technical Report 2000-006, Boston University, January 2000. [ bib | .pdf ] |
[322] | Byron Cook, Christoph Haase, Joël Ouaknine, Matthew J. Parkinson, and James Worrell. Tractable reasoning in a fragment of separation logic. In International Conference on Concurrency Theory (CONCUR), volume 6901 of Lecture Notes in Computer Science, pages 235--249. Springer, September 2011. [ bib | .pdf ] |
[323] | Stephen A. Cook. The complexity of theorem-proving procedures. In ACM Symposium on Theory of Computing, pages 151--158, May 1971. [ bib | http ] |
[324] | William R. Cook. On understanding data abstraction, revisited. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 557--572, October 2009. [ bib | .pdf ] |
[325] | Keith D. Cooper, Timothy J. Harvey, and Ken Kennedy. Iterative data-flow analysis, revisited. Technical Report TR04-432, Rice University, March 2004. [ bib | .pdf ] |
[326] | 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 ] |
[327] | Thierry Coquand. An analysis of Girard's paradox. In Logic in Computer Science (LICS), pages 227--236, June 1986. [ bib | .pdf ] |
[328] | Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. Introduction to algorithms (third edition). MIT Press, 2009. [ bib | http ] |
[329] | Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. Algorithmique (troisième Édition). Sciences Sup. Dunod, 2010. Traduction française. [ bib | http ] |
[330] | Bruno Courcelle. Fundamental properties of infinite trees. Theoretical Computer Science, 25(2):95--169, March 1983. [ bib ] |
[331] | 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 ] |
[332] | Patrick Cousot and Radhia Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Principles of Programming Languages (POPL), pages 238--252, January 1977. [ bib | .pdf ] |
[333] | Patrick Cousot and Radhia Cousot. Constructive versions of Tarski's fixed point theorems. Pacific Journal of Mathematics, 81(1):43--57, 1979. [ bib | .pdf ] |
[334] | Patrick Cousot and Radhia Cousot. Formal language, grammar and set-constraint-based program analysis by abstract interpretation. In Functional Programming Languages and Computer Architecture (FPCA), pages 170--181. ACM Press, 1995. [ bib ] |
[335] | Patrick Cousot and Radhia Cousot. A gentle introduction to formal verification of computer systems by abstract interpretation. In J. Esparza, O. Grumberg, and M. Broy, editors, Logics and Languages for Reliability and Security, NATO Science Series III: Computer and Systems Sciences, pages 1--29. IOS Press, 2010. [ bib | http ] |
[336] | Patrick Cousot, Radhia Cousot, Jérôme Feret, Antoine Miné, and Xavier Rival. The Astrée static analyzer, 2011. http://www.astree.ens.fr/. [ bib | http ] |
[337] | Duncan Coutts, Roman Leshchinskiy, and Don Stewart. Stream fusion: from lists to streams to nothing at all. In International Conference on Functional Programming (ICFP), pages 315--326, October 2007. [ bib | http ] |
[338] | Erik Crank and Matthias Felleisen. Parameter-passing and the lambda calculus. In Principles of Programming Languages (POPL), pages 233--244, January 1991. [ bib | .ps.gz ] |
[339] | Karl Crary. Type-theoretic methodology for practical programming languages. PhD thesis, Cornell University, August 1998. [ bib | .ps.gz ] |
[340] | Karl Crary. Simple, efficient object encoding using intersection types. Technical Report CMU-CS-99-100, Carnegie Mellon University, 1999. [ bib | .ps.gz ] |
[341] | Karl Crary. A simple proof of call-by-value standardization. Technical Report CMU-CS-09-137, Carnegie Mellon University, 2009. [ bib | .pdf ] |
[342] | Karl Crary, David Walker, and Greg Morrisett. Typed memory management in a calculus of capabilities. In Principles of Programming Languages (POPL), pages 262--275, January 1999. [ bib | .pdf ] |
[343] | Karl Crary and Stephanie Weirich. Flexible type analysis. In International Conference on Functional Programming (ICFP), pages 233--248, 1999. [ bib | .ps.gz ] |
[344] | Karl Crary and Stephanie Weirich. Resource bound certification. In Principles of Programming Languages (POPL), pages 184--198, January 2000. [ bib | .pdf ] |
[345] | Karl Crary, Stephanie Weirich, and Greg Morrisett. Intensional polymorphism in type-erasure semantics. In International Conference on Functional Programming (ICFP), pages 301--313, September 1998. [ bib | .ps ] |
[346] | 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 ] |
[347] | Julien Cretin. Erasable coercions: a unified approach to type systems. PhD thesis, Université Paris Diderot, January 2014. [ bib | http ] |
[348] | Julien Cretin and Didier Rémy. On the power of coercion abstraction. In Principles of Programming Languages (POPL), pages 361--372, January 2012. [ bib | .pdf ] |
[349] | Pavel Curtis. Constrained quantification in polymorphic type analysis. PhD thesis, Cornell University, February 1990. [ bib | .ps.gz ] |
[350] | Luis Damas. Type assignment in programming languages. PhD thesis, University of Edinburgh, 1985. [ bib ] |
[351] | Luis Damas and Robin Milner. Principal type-schemes for functional programs. In Principles of Programming Languages (POPL), pages 207--212, 1982. [ bib | http ] |
[352] | 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, 1983. [ bib | http ] |
[353] | Nils Anders Danielsson. Lightweight semiformal time complexity analysis for purely functional data structures. In Principles of Programming Languages (POPL), January 2008. [ bib | .pdf ] |
[354] | Nils Anders Danielsson and Thorsten Altenkirch. Subtyping, declaratively. In Mathematics of Program Construction (MPC), volume 6120 of Lecture Notes in Computer Science, pages 100--118. Springer, June 2010. [ bib | .pdf ] |
[355] | Nils Anders Danielsson, John Hughes, Patrik Jansson, and Jeremy Gibbons. Fast and loose reasoning is morally correct. In Principles of Programming Languages (POPL), pages 206--217, January 2006. [ bib | .pdf ] |
[356] | Norman Danner, Jennifer Paykin, and James S. Royer. A static cost analysis for a higher-order language. In Programming Languages Meets Program Verification (PLPV), pages 25--34, January 2013. [ bib | .pdf ] |
[357] | Olivier Danvy. Functional unparsing. Technical Report RS-98-12, BRICS, May 1998. [ bib | http ] |
[358] | Olivier Danvy. Functional unparsing. Journal of Functional Programming, 8(6):621--625, November 1998. [ bib | http ] |
[359] | Olivier Danvy and Andrzej Filinski. Abstracting control. In ACM Symposium on Lisp and Functional Programming (LFP), pages 151--160, 1990. [ bib | http ] |
[360] | Olivier Danvy and Andrzej Filinski. Representing control: A study of the CPS transformation. Mathematical Structures in Computer Science, 2(4):361--391, 1992. [ bib | http ] |
[361] | Olivier Danvy and Lasse R. Nielsen. Defunctionalization at work. Technical Report RS-01-23, BRICS, June 2001. [ bib | http ] |
[362] | Olivier Danvy and Lasse R. Nielsen. Defunctionalization at work. In Principles and Practice of Declarative Programming (PPDP), pages 162--174, September 2001. [ bib | http ] |
[363] | Olivier Danvy and Lasse R. Nielsen. A first-order one-pass CPS transformation. Theoretical Computer Science, 308(1--3):239--257, 2003. [ bib | http ] |
[364] | Olivier Danvy and Lasse R. Nielsen. CPS transformation of beta-redexes. Technical Report RS-04-39, BRICS, December 2004. [ bib | .pdf ] |
[365] | 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 ] |
[366] | Zaynah Dargaye and Xavier Leroy. Mechanized verification of CPS transformations. In Logic for Programming Artificial Intelligence and Reasoning (LPAR), volume 4790 of Lecture Notes in Artificial Intelligence, pages 211--225. Springer, 2007. [ bib | .pdf ] |
[367] | Rowan Davies. Practical refinement-type checking. Technical Report CMU-CS-05-110, School of Computer Science, Carnegie Mellon University, May 2005. [ bib | .pdf ] |
[368] | Rowan Davies and Frank Pfenning. Intersection types and computational effects. In International Conference on Functional Programming (ICFP), pages 198--208, September 2000. [ bib | .pdf ] |
[369] | Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem-proving. Communications of the ACM, 5(7):394--397, 1962. [ bib | http ] |
[370] | Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM, 7(3):201--215, 1960. [ bib | http ] |
[371] | 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 ] |
[372] | 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, 2006. [ bib | .pdf ] |
[373] | Edsko de Vries, Rinus Plasmeijer, and David Abrahamson. Equality based uniqueness typing. In Trends in Functional Programming (TFP), 2007. [ bib | .pdf ] |
[374] | 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 ] |
[375] | Benjamin Delaware, Bruno C. d. S. Oliveira, and Tom Schrijvers. Meta-theory à la carte. In Principles of Programming Languages (POPL), pages 207--218, January 2013. [ bib | .pdf ] |
[376] | Benjamin Delaware, Steven Keuchel, Tom Schrijvers, and Bruno C. d. S. Oliveira. Modular monadic meta-theory. In International Conference on Functional Programming (ICFP), pages 319--330, September 2013. [ bib | .pdf ] |
[377] | Germán Andrés Delbianco and Aleksandar Nanevski. Hoare-style reasoning with (algebraic) continuations. In International Conference on Functional Programming (ICFP), pages 363--376, September 2013. [ bib | .pdf ] |
[378] | Robert DeLine and Manuel Fähndrich. Enforcing high-level protocols in low-level software. In Programming Language Design and Implementation (PLDI), pages 59--69, June 2001. [ bib | http ] |
[379] | Robert DeLine and Manuel Fähndrich. The Fugue protocol checker: Is your software baroque? Technical Report MSR-TR-2004-07, Microsoft Research, January 2004. [ bib | http ] |
[380] | Robert DeLine and Manuel Fähndrich. Typestates for objects. In European Conference on Object-Oriented Programming (ECOOP), volume 3086 of Lecture Notes in Computer Science, pages 465--490. Springer, June 2004. [ bib | http ] |
[381] | Alan Demers, Susan Horwitz, and Tim Teitelbaum. An efficient general algorithm for dataflow analysis. Acta Informatica, 24(6):679--694, November 1987. [ bib | http ] |
[382] | Peter Dencker, Karl Dürre, and Johannes Heuft. Optimization of parser tables for portable compilers. ACM Transactions on Programming Languages and Systems, 6(4):546--572, 1984. [ bib | http ] |
[383] | Dorothy E. Denning. Cryptography and data security. Addison-Wesley, 1982. [ bib ] |
[384] | 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 ] |
[385] | 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 ] |
[386] | Joel E. Denny and Brian A. Malloy. The IELR(1) algorithm for generating minimal LR(1) parser tables for non-LR(1) grammars with conflict resolution. Science of Computer Programming, 75(11):943--979, 2010. [ bib | http ] |
[387] | 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 ] |
[388] | Franklin L. DeRemer. Simple LR(k) grammars. Communications of the ACM, 14(7):453--460, 1971. [ bib | http ] |
[389] | Franklin Lewis DeRemer. Practical translators for LR(k) languages. Technical Report MIT-LCS-TR-065, Massachusetts Institute of Technology, 1969. [ bib | .pdf ] |
[390] | 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 ] |
[391] | David L. Detlefs, K. Rustan M. Leino, and Greg Nelson. Wrestling with rep exposure. Research Report 156, SRC, July 1998. [ bib | .pdf ] |
[392] | 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 ] |
[393] | Roberto Di Cosmo. Deciding type isomorphisms in a type assignment framework. Journal of Functional Programming, 3(3):485--525, 1993. [ bib | .dvi ] |
[394] | Roberto Di Cosmo. Isomorphisms of types: from λ-calculus to information retrieval and language design. Progress in Theoretical Computer Science. Birkhauser, 1995. [ bib | .html ] |
[395] | Werner Dietl, Sophia Drossopoulou, and Peter Müller. Separating ownership topology and encapsulation with generic universe types. ACM Transactions on Programming Languages and Systems, 33(6):20, 2011. [ bib | .pdf ] |
[396] | Werner Dietl and Peter Müller. Universes: Lightweight ownership for JML. Journal of Object Technology, 4(8):5--32, 2005. [ bib | .pdf ] |
[397] | E. W. Dijkstra. A note on two problems in connection with graphs. Numerische Mathematik, 1:269--271, 1959. [ bib ] |
[398] | Edsger W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM, 18(8):453--457, 1975. [ bib | http ] |
[399] | Allyn Dimock. Type- and flow-directed compilation for specialized data representations. PhD thesis, Harvard University, January 2002. [ bib | .ps.gz ] |
[400] | Allyn Dimock, Ian Westmacott, Robert Muller, Franklyn Turbak, and J. B. Wells. Functioning without closure: type-safe customized function representations for Standard ML. In International Conference on Functional Programming (ICFP), September 2001. [ bib | .ps ] |
[401] | Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew J. Parkinson, and Hongseok Yang. Views: compositional reasoning for concurrent programs. In Principles of Programming Languages (POPL), pages 287--300, January 2013. [ bib | .pdf ] |
[402] | Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew Parkinson, and Viktor Vafeiadis. Concurrent abstract predicates. Technical report, University of Cambridge, Computer Laboratory, April 2010. [ bib | .pdf ] |
[403] | Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkinson, and Viktor Vafeiadis. Concurrent abstract predicates. In European Conference on Object-Oriented Programming (ECOOP), volume 6183 of Lecture Notes in Computer Science, pages 504--528. Springer, 2010. [ bib | .pdf ] |
[404] | Dino Distefano and Matthew J. Parkinson. jStar: towards practical verification for Java. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 213--226, October 2008. [ bib | .pdf ] |
[405] | Robert Dockins, Aquinas Hobor, and Andrew W. Appel. A fresh look at separation algebras and share accounting. In Asian Symposium on Programming Languages and Systems (APLAS), volume 5904 of Lecture Notes in Computer Science, pages 161--177. Springer, December 2009. [ bib | .pdf ] |
[406] | Mike Dodds, Xinyu Feng, Matthew J. Parkinson, and Viktor Vafeiadis. Deny-guarantee reasoning. In European Symposium on Programming (ESOP), volume 5502 of Lecture Notes in Computer Science, pages 363--377. Springer, March 2009. [ bib | .pdf ] |
[407] | Mike Dodds, Suresh Jagannathan, and Matthew J. Parkinson. Modular reasoning for deterministic parallelism. In Principles of Programming Languages (POPL), pages 259--270, January 2011. [ bib | .pdf ] |
[408] | Mike Dodds, Suresh Jagannathan, Matthew J. Parkinson, Kasper Svendsen, and Lars Birkedal. Verifying custom synchronization constructs using higher-order separation logic. ACM Transactions on Programming Languages and Systems, 28(2), January 2016. [ bib | http ] |
[409] | Stephen Dolan, K. C. Sivaramakrishnan, and Anil Madhavapeddy. Bounding data races in space and time. In Programming Language Design and Implementation (PLDI), pages 242--255, June 2018. [ bib | .pdf ] |
[410] | Charles Donnelly and Richard Stallman. Bison, January 2015. [ bib | http ] |
[411] | 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 ] |
[412] | Vincent Dornic, Pierre Jouvelot, and David K. Gifford. Polymorphic time systems for estimating program complexity. ACM Letters on Programming Languages and Systems, 1(1):33--45, 1992. [ bib | .pdf ] |
[413] | 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 ] |
[414] | Gilles Dowek, Thérèse Hardin, and Claude Kirchner. Higher order unification via explicit substitutions. Research Report 2709, INRIA, November 1995. [ bib | .html ] |
[415] | 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 ] |
[416] | William F. Dowling and Jean H. Gallier. Linear-time algorithms for testing the satisfiability of propositional Horn formulae. Journal of Logic Programming, 1(3):267--284, 1984. [ bib ] |
[417] | 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 ] |
[418] | Derek Dreyer, Georg Neis, and Lars Birkedal. The impact of higher-order state and control effects on local relational reasoning. In International Conference on Functional Programming (ICFP), pages 143--156, September 2010. [ bib | .pdf ] |
[419] | 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 ] |
[420] | 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 | .pdf ] |
[421] | Dominic Duggan and Frederick Bent. Explaining type inference. Science of Computer Programming, 27(1), June 1996. [ bib ] |
[422] | 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, September 1995. [ bib | .dvi.gz ] |
[423] | Kent Dybvig, Robert Hieb, and Carl Bruggeman. Syntactic abstraction in Scheme. Lisp and Symbolic Computation, 5(4):295--326, 1993. [ bib | .pdf ] |
[424] | Manuel Eberl. Proving divide and conquer complexities in Isabelle/HOL. Journal of Automated Reasoning, 58(4):483--508, 2017. [ bib | .pdf ] |
[425] | Jonathan Eifrig, Scott Smith, and Valery Trifonov. Sound polymorphic type inference for objects. ACM SIGPLAN Notices, 30(10):169--184, 1995. [ bib | .ps.gz ] |
[426] | 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 ] |
[427] | E. Allen Emerson and Chin-Laung Lei. Efficient model checking in fragments of the propositional mu-calculus. In Logic in Computer Science (LICS), pages 267--278, June 1986. [ bib ] |
[428] | 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 ] |
[429] | Ú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 ] |
[430] | Ú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 ] |
[431] | Javier Esparza, David Hansel, Peter Rossmanith, and Stefan Schwoon. Efficient algorithms for model checking pushdown systems. In Computer Aided Verification (CAV), volume 1855 of Lecture Notes in Computer Science, pages 232--247. Springer, July 2000. [ bib | .pdf ] |
[432] | Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, and Jan-Georg Smaus. A fully verified executable LTL model checker. In Computer Aided Verification (CAV), volume 8044 of Lecture Notes in Computer Science, pages 463--478. Springer, July 2013. [ bib | .pdf ] |
[433] | Sylvain Conchon et Jean-Christophe Filliâtre. Apprendre à programmer avec OCaml: Algorithmes et structures de données. Eyrolles, 2014. [ bib | http ] |
[434] | Karl-Filip Faxén. A static semantics for Haskell. Journal of Functional Programming, 12(4--5):295--357, July 2002. [ bib | .ps.gz ] |
[435] | 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 ] |
[436] | J. S. Fenton. Information protection systems. PhD thesis, University of Cambridge, 1973. [ bib ] |
[437] | J. S. Fenton. Memoryless subsystems. Computer Journal, 17(2):143--147, May 1974. [ bib ] |
[438] | Francisco Ferreira and Brigitte Pientka. Programs using syntax with first-class binders. In European Symposium on Programming (ESOP), volume 10201 of Lecture Notes in Computer Science, pages 504--529. Springer, April 2017. [ bib | .pdf ] |
[439] | 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 ] |
[440] | Andrzej Filinski. Representing layered monads. In Principles of Programming Languages (POPL), pages 175--188, January 1999. [ bib | .ps.gz ] |
[441] | Jean-Christophe Filliâtre. Backtracking iterators. In ACM Workshop on ML, pages 55--62, September 2006. [ bib | .ps.gz ] |
[442] | Jean-Christophe Filliâtre and Sylvain Conchon. Type-safe modular hash-consing. In ACM Workshop on ML, pages 12--19, September 2006. [ bib | .pdf ] |
[443] | Jean-Christophe Filliâtre, Léon Gondelman, and Andrei Paskevich. The spirit of ghost code. In Computer Aided Verification (CAV), volume 8559 of Lecture Notes in Computer Science, pages 1--16. Springer, July 2014. [ bib | .pdf ] |
[444] | Jean-Christophe Filliâtre and Andrei Paskevich. Why3---where programs meet provers. In European Symposium on Programming (ESOP), volume 7792 of Lecture Notes in Computer Science, pages 125--128. Springer, March 2013. [ bib | http ] |
[445] | Jean-Christophe Filliâtre and Mário Pereira. A modular way to reason about iteration. In NASA Formal Methods (NFM), volume 9690 of Lecture Notes in Computer Science, pages 322--336. Springer, June 2016. [ bib | http ] |
[446] | 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 ] |
[447] | Jean-Christophe Filliâtre. Why: a multi-language multi-prover verification tool. Research Report 1366, LRI, Université Paris Sud, March 2003. [ bib | .ps.gz ] |
[448] | Jean-Christophe Filliâtre. Formal proof of a program: Find. Science of Computer Programming, 64:332--240, 2006. [ bib | .ps.gz ] |
[449] | 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, March 2004. [ bib | http ] |
[450] | 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, November 2004. [ bib | .ps.gz ] |
[451] | Jean-Christophe Filliâtre and Claude Marché. The Why/Krakatoa/Caduceus platform for deductive program verification. In Computer Aided Verification (CAV), volume 4590 of Lecture Notes in Computer Science, pages 173--177. Springer, July 2007. [ bib | .pdf ] |
[452] | Robert Bruce Findler and Matthias Felleisen. Contracts for higher-order functions. In International Conference on Functional Programming (ICFP), pages 48--59, October 2002. [ bib | .pdf ] |
[453] | Adam Fischbach and John Hannan. Specification and correctness of lambda lifting. Journal of Functional Programming, 13(3):509--543, May 2003. [ bib | http ] |
[454] | Michael J. Fischer. Lambda calculus schemata. In Proceedings of the ACM Conference on Proving Assertions About Programs, pages 104--109, 1972. [ bib | http ] |
[455] | Michael J. Fischer. Lambda-calculus schemata. Lisp and Symbolic Computation, 6(3--4):259--288, 1993. [ bib | http ] |
[456] | 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 ] |
[457] | Cormac Flanagan. Effective static debugging via componential set-based analysis. PhD thesis, Rice University, May 1997. [ bib | .ps.gz ] |
[458] | Cormac Flanagan and Martín Abadi. Types for safe locking. In European Symposium on Programming (ESOP), volume 1576 of Lecture Notes in Computer Science, pages 91--108. Springer, March 1999. [ bib | .pdf ] |
[459] | 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 ] |
[460] | Cormac Flanagan and Matthias Felleisen. Componential set-based analysis. In Programming Language Design and Implementation (PLDI), pages 235--248, 1997. [ bib | .ps.gz ] |
[461] | Cormac Flanagan, Matthew Flatt, Shriram Krishnamurthi, Stephanie Weirich, and Matthias Felleisen. Catching bugs in the web of program invariants. In Programming Language Design and Implementation (PLDI), 1996. [ bib | .ps.gz ] |
[462] | Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata. Extended static checking for Java. In Programming Language Design and Implementation (PLDI), pages 234--245, 2002. [ bib | .ps ] |
[463] | Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The essence of compiling with continuations. In Programming Language Design and Implementation (PLDI), pages 237--247, 1993. [ bib | .pdf ] |
[464] | Cormac Flanagan and James B. Saxe. Avoiding exponential explosion: generating compact verification conditions. In Principles of Programming Languages (POPL), pages 193--205, 2001. [ bib | .ps ] |
[465] | 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 | .pdf ] |
[466] | Matthew Fluet. Monadic and substructural type systems for region-based memory management. PhD thesis, Cornell University, January 2007. [ bib | .pdf ] |
[467] | Matthew Fluet and Greg Morrisett. Monadic regions. Journal of Functional Programming, 16(4--5):485--545, 2006. [ bib | http ] |
[468] | 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, March 2006. [ bib | .pdf ] |
[469] | 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 ] |
[470] | 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 ] |
[471] | 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 ] |
[472] | 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 ] |
[473] | Bryan Ford. Packrat parsing: simple, powerful, lazy, linear time. In International Conference on Functional Programming (ICFP), pages 36--47, October 2002. [ bib | .pdf ] |
[474] | Bryan Ford. Parsing expression grammars: a recognition-based syntactic foundation. In Principles of Programming Languages (POPL), pages 111--122, January 2004. [ bib | .pdf ] |
[475] | 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 ] |
[476] | Jeffrey S. Foster, Tachio Terauchi, and Alex Aiken. Flow-sensitive type qualifiers. In Programming Language Design and Implementation (PLDI), pages 1--12, June 2002. [ bib | .pdf ] |
[477] | Cédric Fournet and Georges Gonthier. The reflexive chemical abstract machine and the join-calculus. In Principles of Programming Languages (POPL), pages 372--385, January 1996. [ bib | http ] |
[478] | Cédric Fournet and Andrew D. Gordon. Stack inspection: Theory and variants. In Principles of Programming Languages (POPL), pages 307--318, January 2002. [ bib | .ps ] |
[479] | 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 ] |
[480] | Cédric Fournet, Cosimo Laneve, Luc Maranget, and Didier Rémy. Inheritance in the join calculus. Journal of Logic and Algebraic Programming, 57(2):23--69, 2003. [ bib | .pdf ] |
[481] | 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, 1997. [ bib | .pdf ] |
[482] | Adrian Francalanza, Julian Rathke, and Vladimiro Sassone. Permission-based separation logic for message-passing concurrency. Logical Methods in Computer Science, 7(3), 2011. [ bib | http ] |
[483] | Michael Fredman and Michael Saks. The cell probe complexity of dynamic data structures. In Annual Symposium on Theory of Computing (STOC), pages 345--354. ACM, May 1989. [ bib | http ] |
[484] | Michael L. Fredman and Robert Endre Tarjan. Fibonacci heaps and their uses in improved network optimization algorithms. Journal of the ACM, 34(3):596--615, 1987. [ bib | http ] |
[485] | Tim Freeman and Frank Pfenning. Refinement types for ML. In Programming Language Design and Implementation (PLDI), pages 268--277, 1991. [ bib | .pdf ] |
[486] | 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, September 1997. [ bib | .html ] |
[487] | 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 ] |
[488] | Daniel P. Friedman and Mitchell Wand. Essentials of programming languages, 3rd edition. MIT Press, 2008. [ bib | http ] |
[489] | Matteo Frigo and Steven G. Johnson. The design and implementation of FFTW3. Proceedings of the IEEE, 93(2):216--231, 2005. [ bib | .pdf ] |
[490] | Alain Frisch, Giuseppe Castagna, and Véronique Benzaken. Semantic subtyping. In Logic in Computer Science (LICS), pages 137--146, July 2002. [ bib | .ps.gz ] |
[491] | Alain Frisch, Giuseppe Castagna, and Véronique Benzaken. Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types. Journal of the ACM, 55(4), 2008. [ bib | .pdf ] |
[492] | 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, 1988. [ bib | http ] |
[493] | You-Chin Fuh and Prateek Mishra. Polymorphic subtype inference: Closing the theory-practice gap. In Theory and Practice of Software Development (TAPSOFT), volume 352 of Lecture Notes in Computer Science, pages 167--183. Springer, March 1989. [ bib | http ] |
[494] | 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, November 2003. [ bib | .ps.gz ] |
[495] | 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 ] |
[496] | Manuel Fähndrich. Bane: A library for scalable constraint-based program analysis. PhD thesis, University of California at Berkeley, 1999. [ bib | .pdf ] |
[497] | 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 ] |
[498] | Manuel Fähndrich and Robert DeLine. Adoption and focus: practical linear types for imperative programming. In Programming Language Design and Implementation (PLDI), pages 13--24, June 2002. [ bib | .pdf ] |
[499] | Manuel Fähndrich, Jeffrey S. Foster, Zhendong Su, and Alexander S. Aiken. Partial online cycle elimination in inclusion constraint graphs. In Programming Language Design and Implementation (PLDI), pages 85--96, June 1998. [ bib | .pdf ] |
[500] | Manuel Fähndrich and Rustan Leino. Heap monotonic typestates. In International Workshop on Alias Confinement and Ownership (IWACO), July 2003. [ bib | .pdf ] |
[501] | Manuel Fähndrich, Jakob Rehof, and Manuvir Das. Scalable context-sensitive flow analysis using instantiation constraints. In Programming Language Design and Implementation (PLDI), June 2000. [ bib | .ps ] |
[502] | Murdoch J. Gabbay. A theory of inductive definitions with α-equivalence. PhD thesis, Cambridge University, 2001. [ bib | .pdf ] |
[503] | Murdoch J. Gabbay. A general mathematics of names in syntax. Submitted for publication, March 2004. [ bib | .pdf ] |
[504] | 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 ] |
[505] | Zvi Galil and Giuseppe F. Italiano. Data structures and algorithms for disjoint set union problems. ACM Computing Surveys, 23(3):319--344, 1991. [ bib | http ] |
[506] | Bernard A. Galler and Michael J. Fischer. An improved equivalence algorithm. Communications of the ACM, 7(5):301--303, 1964. [ bib | http ] |
[507] | Erich Gamma, Richard Helm, Ralph Johnson, and John Vlissides. Design patterns: Elements of reusable object-oriented software. Addison-Wesley, 1995. [ bib ] |
[508] | Vladimir Gapeyev, Michael Levin, and Benjamin Pierce. Recursive subtyping revealed. Journal of Functional Programming, 12(6):511--548, November 2002. [ bib | http ] |
[509] | Philippa Gardner, Gian Ntzik, and Adam Wright. Local reasoning for the POSIX file system. In European Symposium on Programming (ESOP), volume 8410 of Lecture Notes in Computer Science, pages 169--188. Springer, April 2014. [ bib | .pdf ] |
[510] | 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 ] |
[511] | Jacques Garrigue. Programming with polymorphic variants. In ACM Workshop on ML, September 1998. [ bib | .ps.gz ] |
[512] | Jacques Garrigue. Code reuse through polymorphic variants. In Workshop on Foundations of Software Engineering, November 2000. [ bib | .ps.gz ] |
[513] | Jacques Garrigue. Simple type inference for structural polymorphism. In Foundations of Object-Oriented Languages (FOOL), January 2002. [ bib | .ps.gz ] |
[514] | Jacques Garrigue. Relaxing the value restriction. In Functional and Logic Programming, volume 2998 of Lecture Notes in Computer Science, pages 196--213. Springer, April 2004. [ bib | .pdf ] |
[515] | Jacques Garrigue. A certified implementation of ML with structural polymorphism and recursive types. Mathematical Structures in Computer Science, 25(4):867--891, 2015. [ bib | .pdf ] |
[516] | Jacques Garrigue and Didier Rémy. Extending ML with semi-explicit higher-order polymorphism. Information and Computation, 155(1):134--169, 1999. [ bib | .pdf ] |
[517] | Jacques Garrigue and Didier Rémy. Ambivalent types for principal type inference with GADTs. In Asian Symposium on Programming Languages and Systems (APLAS), December 2013. [ bib | .pdf ] |
[518] | Benedict R. Gaster. Records, variants and qualified types. PhD thesis, University of Nottingham, July 1998. [ bib | .ps ] |
[519] | 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 ] |
[520] | Nadji Gauthier and François Pottier. Numbering matters: First-order canonical forms for second-order recursive types. In International Conference on Functional Programming (ICFP), pages 150--161, September 2004. [ bib | .pdf ] |
[521] | Simon J. Gay, Vasco Thudichum Vasconcelos, António Ravara, Nils Gesbert, and Alexandre Z. Caldeira. Modular session types for distributed object-oriented programming. In Principles of Programming Languages (POPL), pages 299--312, January 2010. [ bib | .pdf ] |
[522] | 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, 1983. [ bib | http ] |
[523] | 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 ] |
[524] | Giorgio Ghelli. Divergence of F_{<=} type checking. Theoretical Computer Science, 139(1--2):131--162, March 1995. [ bib | .ps.gz ] |
[525] | Cristian Gherghina, Cristina David, Shengchao Qin, and Wei-Ngan Chin. Structured specifications for better verification of heap-manipulating programs. In Formal Methods (FM), volume 6664 of Lecture Notes in Computer Science, pages 386--401. Springer, June 2011. [ bib | .pdf ] |
[526] | Jeremy Gibbons. Datatype-generic programming. In International Spring School on Datatype-Generic Programming, volume 4719 of Lecture Notes in Computer Science, pages 1--71. Springer, April 2006. [ bib | .pdf ] |
[527] | Jürgen Giesl, Cornelius Aschermann, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Jera Hensel, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephanie Swiderski, and René Thiemann. Analyzing program termination and complexity automatically with AProVE. Journal of Automated Reasoning, 58(1):3--31, 2017. [ bib | .pdf ] |
[528] | 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 ] |
[529] | 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 ] |
[530] | 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 ] |
[531] | Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1--102, 1987. [ bib | .pdf ] |
[532] | Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and types. Cambridge University Press, 1990. [ bib | .pdf ] |
[533] | Neal Glew. Object closure conversion. In Higher Order Operational Techniques in Semantics (HOOTS), volume 26 of Electronic Notes in Theoretical Computer Science, pages 52--68, September 1999. [ bib | .ps.gz ] |
[534] | Neal Glew. An efficient class and object encoding. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 311--324, October 2000. [ bib | .ps.gz ] |
[535] | 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, April 2002. [ bib | .pdf ] |
[536] | 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, 1985. [ bib | http ] |
[537] | 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 ] |
[538] | Li Gong, Gary Ellison, and Mary Dageforde. Inside Java 2 platform security, second edition. Addison-Wesley, 2003. [ bib | http ] |
[539] | 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 ] |
[540] | 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 ] |
[541] | Andrew D. Gordon and Tom Melham. Five axioms of alpha-conversion. In Theorem Proving in Higher Order Logics (TPHOLs), volume 1125 of Lecture Notes in Computer Science, pages 173--191. Springer, August 1996. [ bib | .ps.gz ] |
[542] | Colin S. Gordon, Matthew J. Parkinson, Jared Parsons, Aleks Bromfield, and Joe Duffy. Uniqueness and reference immutability for safe parallelism. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 21--40, October 2012. [ bib | .pdf ] |
[543] | Donald Gordon and James Noble. Dynamic ownership in a dynamic language. In Symposium on Dynamic Languages, pages 41--52, 2007. [ bib | http ] |
[544] | James Gosling, Bill Joy, Guy Steele, and Gilad Bracha. The Java language specification, second edition. Addison-Wesley, 2000. [ bib | http ] |
[545] | Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, and Mooly Sagiv. Local reasoning for storable locks and threads. In Asian Symposium on Programming Languages and Systems (APLAS), volume 4807 of Lecture Notes in Computer Science, pages 19--37. Springer, November 2007. [ bib | http ] |
[546] | 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 ] |
[547] | Jean Goubault. Inférence d'unités physiques en ML. In Journées Françaises des Langages Applicatifs (JFLA), pages 3--20, 1994. [ bib ] |
[548] | Ronald L. Graham, Donald E. Knuth, and Oren Patashnik. Concrete mathematics: a foundation for computer science. Addison-Wesley, 1994. [ bib | .html ] |
[549] | David Gries. Describing an algorithm by Hopcroft. Acta Informatica, 2:97--109, 1973. [ bib | http ] |
[550] | Jessica Gronski, Kenneth Knowles, Aaron Tomb, Stephen N. Freund, and Cormac Flanagan. Sage: Hybrid checking for flexible specifications. In Scheme and Functional Programming, pages 93--104, September 2006. [ bib | .pdf ] |
[551] | Josef Grosch. Efficient and comfortable error recovery in recursive descent parsers. Structured Programming, 11(3):129--140, 1990. [ bib | .pdf ] |
[552] | Dan Grossman. Quantified types in an imperative language. ACM Transactions on Programming Languages and Systems, 28(3):429--475, May 2006. [ bib | .pdf ] |
[553] | Dan Grossman, Greg Morrisett, Trevor Jim, Michael Hicks, Yanling Wang, and James Cheney. Region-based memory management in Cyclone. In Programming Language Design and Implementation (PLDI), pages 282--293, June 2002. [ bib | .pdf ] |
[554] | Dick Grune and Ceriel J. H. Jacobs. Parsing techniques: a practical guide. Ellis Horwood, 1990. [ bib | .html ] |
[555] | Dick Grune and Ceriel J. H. Jacobs. Parsing techniques: a practical guide, second edition. Monographs in computer science. Springer, 2008. [ bib | .html ] |
[556] | Louis-Julien Guillemette and Stefan Monnier. A type-preserving closure conversion in Haskell. In Haskell workshop, pages 83--92, September 2007. [ bib | .pdf ] |
[557] | Louis-Julien Guillemette and Stefan Monnier. Type-safe code transformations in Haskell. Electronic Notes in Theoretical Computer Science, 174(7):23--39, 2007. [ bib | http ] |
[558] | Louis-Julien Guillemette and Stefan Monnier. One vote for type families in Haskell! In Trends in Functional Programming (TFP), 2008. [ bib | .pdf ] |
[559] | Louis-Julien Guillemette and Stefan Monnier. A type-preserving compiler in Haskell. In International Conference on Functional Programming (ICFP), pages 75--86, September 2008. [ bib | .pdf ] |
[560] | Sumit Gulwani. SPEED: symbolic complexity bound analysis. In Computer Aided Verification (CAV), volume 5643 of Lecture Notes in Computer Science, pages 51--62. Springer, July 2009. [ bib | http ] |
[561] | Sumit Gulwani, Krishna K. Mehra, and Trishul M. Chilimbi. SPEED: precise and efficient static estimation of program computational complexity. In Principles of Programming Languages (POPL), pages 127--139, January 2009. [ bib | http ] |
[562] | Adam Gundry. Type inference, Haskell and dependent types. PhD thesis, University of Strathclyde, 2013. [ bib | .pdf ] |
[563] | Adam Gundry, Conor McBride, and James McKinna. Type inference in context. In Workshop on Mathematically Structured Functional Programming (MSFP), pages 43--54, September 2010. [ bib | .pdf ] |
[564] | Kartik Gupta and V. Krishna Nandivada. Lexical state analyzer for JavaCC grammars. Software: Practice and Experience, 2015. [ bib | http ] |
[565] | Jörgen Gustavsson and Josef Svenningsson. Constraint abstractions. In Symposium on Programs as Data Objects, volume 2053 of Lecture Notes in Computer Science. Springer, May 2001. [ bib | .pdf ] |
[566] | 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 ] |
[567] | Armaël Guéneau, Arthur Charguéraud, and François Pottier. A fistful of dollars: Formalizing asymptotic complexity claims via deductive program verification. In European Symposium on Programming (ESOP), volume 10801 of Lecture Notes in Computer Science, pages 533--560. Springer, April 2018. [ bib | .pdf ] |
[568] | Armaël Guéneau, Magnus O. Myreen, Ramana Kumar, and Michael Norrish. Verified characteristic formulae for CakeML. In European Symposium on Programming (ESOP), volume 10201 of Lecture Notes in Computer Science, pages 584--610. Springer, April 2017. [ bib | .pdf ] |
[569] | Armaël Guéneau, François Pottier, and Jonathan Protzenko. The ins and outs of iteration in Mezzo. Higher-Order Programming and Effects (HOPE), September 2013. http://goo.gl/NrgKc4. [ bib ] |
[570] | Christian Haack, Marieke Huisman, and Clément Hurlin. Reasoning about Java's reentrant locks. In Asian Symposium on Programming Languages and Systems (APLAS), volume 5356 of Lecture Notes in Computer Science, pages 171--187. Springer, December 2008. [ bib | .pdf ] |
[571] | Christian Haack and Clément Hurlin. Resource usage protocols for iterators. Journal of Object Technology, 8(4):55--83, 2009. [ bib | .pdf ] |
[572] | 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, 2003. [ bib | .pdf ] |
[573] | 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, April 1994. [ bib | .ps.gz ] |
[574] | 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 ] |
[575] | Philipp Haller and Martin Odersky. Capabilities for uniqueness and borrowing. In European Conference on Object-Oriented Programming (ECOOP), volume 6183 of Lecture Notes in Computer Science, pages 354--378. Springer, June 2010. [ bib | .pdf ] |
[576] | 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 ] |
[577] | 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 ] |
[578] | Michael Hanus. Horn clause specifications with polymorphic types. PhD thesis, Fachbereich Informatik, Universität Dortmund, 1988. [ bib | .dvi.Z ] |
[579] | Michael Hanus. Horn clause programs with polymorphic types: Semantics and resolution. In Theory and Practice of Software Development (TAPSOFT), volume 352 of Lecture Notes in Computer Science, pages 225--240. Springer, 1989. [ bib | .ps ] |
[580] | Norm Hardy. The confused deputy (or why capabilities might have been invented). ACM Operating Systems Review, 22(4):36--38, October 1988. [ bib | .html ] |
[581] | Gregory C. Harfst and Edward M. Reingold. A potential-based amortized analysis of the union-find data structure. SIGACT News, 31(3):86--95, 2000. [ bib | http ] |
[582] | Bob Harper and Mark Lillibridge. ML with callcc is unsound. Message to the TYPES mailing list, July 1991. [ bib | .html ] |
[583] | Robert Harper. A simplified account of polymorphic references. Information Processing Letters, 51(4):201--206, 1994. [ bib | .pdf ] |
[584] | Robert Harper. Proof-directed debugging. Journal of Functional Programming, 9(4):463--469, 1999. [ bib | http ] |
[585] | Robert Harper, Furio Honsell, and Gordon D. Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143--184, 1993. [ bib | .pdf ] |
[586] | Robert Harper and Daniel R. Licata. Mechanizing metatheory in a logical framework. Journal of Functional Programming, 17(4--5):613--673, 2007. [ bib | .pdf ] |
[587] | Robert Harper and Mark Lillibridge. Polymorphic type assignment and CPS conversion. Lisp and Symbolic Computation, 6(3--4):361--380, 1993. [ bib | .pdf ] |
[588] | Robert Harper and Benjamin Pierce. A record calculus based on symmetric concatenation. In Principles of Programming Languages (POPL), pages 131--142, January 1991. [ bib | .ps ] |
[589] | Robert Harper and Benjamin C. Pierce. Design considerations for ML-style module systems. In Benjamin C. Pierce, editor, Advanced Topics in Types and Programming Languages, chapter 8, pages 293--345. MIT Press, 2005. [ bib ] |
[590] | John Harrison. Handbook of practical logic and automated reasoning. Cambridge University Press, 2009. [ bib | http ] |
[591] | 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 ] |
[592] | Maximilian P. L. Haslbeck and Tobias Nipkow. Hoare logics for time bounds: A study in meta theory. In Tools and Algorithms for Construction and Analysis of Systems (TACAS), volume 10805 of Lecture Notes in Computer Science, pages 155--171. Springer, April 2018. [ bib | .pdf ] |
[593] | Chris Hawblitzel. Linear types for aliased resources. Technical Report MSR-TR-2005-141, Microsoft Research, October 2005. [ bib | .pdf ] |
[594] | Matthew S. Hecht and Jeffrey D. Ullman. Analysis of a simple algorithm for global data flow problems. In Principles of Programming Languages (POPL), pages 207--217, 1973. [ bib | http ] |
[595] | 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 ] |
[596] | 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 ] |
[597] | 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 ] |
[598] | Eric C. R. Hehner. Abstractions of time, pages 191--210. Prentice Hall, 1994. [ bib | .pdf ] |
[599] | Eric C. R. Hehner. Formalization of time and space. Formal Aspects of Computing, 10:290--206, 1998. [ bib | .pdf ] |
[600] | 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 ] |
[601] | Nevin Heintze and David McAllester. Linear-time subtransitive control flow analysis. In Programming Language Design and Implementation (PLDI), pages 261--272, 1997. [ bib | .ps ] |
[602] | Nevin Heintze and Jon G. Riecke. The SLam calculus: Programming with secrecy and integrity. In Principles of Programming Languages (POPL), pages 365--377, January 1998. [ bib | .ps ] |
[603] | Nevin Heintze and Olivier Tardieu. Ultra-fast aliasing analysis using CLA: A million lines of C code in a second. In Programming Language Design and Implementation (PLDI), pages 254--263, 2001. [ bib | .ps ] |
[604] | Simon Helsen and Peter Thiemann. Syntactic type soundness for the region calculus. In Higher Order Operational Techniques in Semantics (HOOTS), volume 41(3) of Electronic Notes in Theoretical Computer Science, pages 1--19, 2000. [ bib | .pdf ] |
[605] | Fergus Henderson. Strong modes can change the world! Technical Report 96/11, Department of Computer Science, University of Melbourne, November 1992. [ bib | .ps.gz ] |
[606] | 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, 2003. [ bib | http ] |
[607] | Fritz Henglein. Polymorphic type inference and semi-unification. PhD thesis, Rutgers University, April 1989. [ bib | .ps.gz ] |
[608] | Fritz Henglein. Efficient type inference for higher-order binding-time analysis. In Functional Programming Languages and Computer Architecture (FPCA), volume 523 of Lecture Notes in Computer Science, pages 448--472. Springer, 1991. [ bib | .dvi.gz ] |
[609] | Fritz Henglein. Type inference with polymorphic recursion. ACM Transactions on Programming Languages and Systems, 15(2):253--289, April 1993. [ bib | http ] |
[610] | Fritz Henglein. Breaking through the n^{3} barrier: Faster object type inference. In Foundations of Object-Oriented Languages (FOOL), 1997. [ bib ] |
[611] | Fritz Henglein. Breaking through the n^{3} barrier: Faster object type inference. Theory and Practice of Object Systems, 5(1):57--72, 1999. [ bib | .ps.gz ] |
[612] | Fritz Henglein and Jakob Rehof. The complexity of subtype entailment for simple types. In Logic in Computer Science (LICS), pages 352--361, June 1997. [ bib | .ps ] |
[613] | 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 ] |
[614] | Matthew Hennessy. The security picalculus and non-interference. Technical Report 2000:05, University of Sussex, November 2000. [ bib | .ps.Z ] |
[615] | 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, July 2000. [ bib | .ps.gz ] |
[616] | Mark Hepburn and David Wright. Trust in the pi-calculus. In Principles and Practice of Declarative Programming (PPDP), September 2001. [ bib ] |
[617] | Brian Herlihy, Peter Schachte, and Harald Søndergaard. Un-Kleene Boolean equation solving. International Journal of Foundations of Computer Science, 18(2):227--250, 2007. [ bib | http ] |
[618] | Stefan Heule, K. Rustan M. Leino, Peter Müller, and Alexander J. Summers. Abstract read permissions: Fractional permissions without the fractions. In Verification, Model Checking and Abstract Interpretation (VMCAI), volume 7737 of Lecture Notes in Computer Science, pages 315--334. Springer, 2013. [ bib | .pdf ] |
[619] | Tomoyuki Higuchi and Atsushi Ohori. A static type system for JVM access control. In International Conference on Functional Programming (ICFP), pages 227--237, August 2003. [ bib | http ] |
[620] | Daniel Hillerström and Sam Lindley. Liberating effects with rows and handlers. In International Workshop on Type-Driven Development (TyDe@ICFP), pages 15--27, September 2016. [ bib | .pdf ] |
[621] | 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 ] |
[622] | 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 ] |
[623] | Ralf Hinze, Johan Jeuring, and Andres Löh. Comparing approaches to generic programming in Haskell. Technical Report UU-CS-2006-022, Department of Information and Computing Sciences, Utrecht University, 2006. [ bib | .pdf ] |
[624] | Ralf Hinze and Andres Löh. “scrap your boilerplate” revolutions. In Mathematics of Program Construction (MPC), volume 4014 of Lecture Notes in Computer Science, pages 180--208. Springer, July 2006. [ bib | .pdf ] |
[625] | Ralf Hinze, Andres Löh, and Bruno C. d. S. Oliveira. “scrap your boilerplate” reloaded. In Functional and Logic Programming, volume 3945 of Lecture Notes in Computer Science, pages 13--29. Springer, April 2006. [ bib | .pdf ] |
[626] | Ralf Hinze and Ross Paterson. Derivation of a typed functional LR parser. Unpublished, November 2005. [ bib | .pdf ] |
[627] | Ralf Hinze and Ross Paterson. Finger trees: a simple general-purpose data structure. Journal of Functional Programming, 16(2):197--217, 2006. [ bib | .pdf ] |
[628] | Ralf Hinze and Simon Peyton Jones. Derivable type classes. In Haskell workshop, 2000. [ bib | .pdf ] |
[629] | 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 ] |
[630] | 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, April 2004. [ bib | .ps.gz ] |
[631] | My Hoang and John C. Mitchell. Lower bounds on type inference with subtypes. In Principles of Programming Languages (POPL), pages 176--185, January 1995. [ bib | http ] |
[632] | C. A. R. Hoare. Algorithm 65: find. Communications of the ACM, 4(7):321--322, July 1961. [ bib | http ] |
[633] | C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576--580, 1969. [ bib | http ] |
[634] | C. A. R. Hoare. Proof of a program: FIND. Communications of the ACM, 14(1):39--45, January 1971. [ bib | http ] |
[635] | C. A. R. Hoare. Proof of correctness of data representations. Acta Informatica, 4:271--281, 1972. [ bib | http ] |
[636] | Aquinas Hobor, Andrew W. Appel, and Francesco Zappa Nardelli. Oracle semantics for concurrent separation logic. In European Symposium on Programming (ESOP), volume 4960 of Lecture Notes in Computer Science, pages 353--367. Springer, April 2008. [ bib | .pdf ] |
[637] | Aquinas Hobor, Robert Dockins, and Andrew W. Appel. A theory of indirection via approximation. In Principles of Programming Languages (POPL), January 2010. [ bib | .pdf ] |
[638] | Aquinas Hobor and Cristian Gherghina. Barriers in concurrent separation logic. In European Symposium on Programming (ESOP), Lecture Notes in Computer Science. Springer, March 2011. [ bib | .pdf ] |
[639] | Jan Hoffmann, Klaus Aehlig, and Martin Hofmann. Multivariate amortized resource analysis. ACM Transactions on Programming Languages and Systems, 34(3):14:1--14:62, 2012. [ bib | http ] |
[640] | Jan Hoffmann, Klaus Aehlig, and Martin Hofmann. Resource aware ML. In Computer Aided Verification (CAV), volume 7358 of Lecture Notes in Computer Science, pages 781--786. Springer, July 2012. [ bib | http ] |
[641] | Jan Hoffmann, Ankush Das, and Shu-Chun Weng. Towards automatic resource bound analysis for OCaml. In Principles of Programming Languages (POPL), pages 359--373, January 2017. [ bib | .pdf ] |
[642] | Jan Hoffmann and Martin Hofmann. Amortized resource analysis with polynomial potential. In European Symposium on Programming (ESOP), volume 6012 of Lecture Notes in Computer Science, pages 287--306. Springer, March 2010. [ bib | .pdf ] |
[643] | Jan Hoffmann, Michael Marmar, and Zhong Shao. Quantitative reasoning for proving lock-freedom. In Logic in Computer Science (LICS), pages 124--133, June 2013. [ bib | .pdf ] |
[644] | Martin Hofmann. A type system for bounded space and functional in-place update. Nordic Journal of Computing, 7(4):258--289, 2000. [ bib | .ps.gz ] |
[645] | Martin Hofmann and Steffen Jost. Static prediction of heap space usage for first-order functional programs. In Principles of Programming Languages (POPL), pages 185--197, January 2003. [ bib | .pdf ] |
[646] | Martin Hofmann, Aleksandr Karbyshev, and Helmut Seidl. Verifying a local generic solver in Coq. In Static Analysis Symposium (SAS), volume 6337 of Lecture Notes in Computer Science, pages 340--355. Springer, September 2010. [ bib | .pdf ] |
[647] | Martin Hofmann, Aleksandr Karbyshev, and Helmut Seidl. What is a pure functional? In International Colloquium on Automata, Languages and Programming, volume 6199 of Lecture Notes in Computer Science, pages 199--210. Springer, July 2010. [ bib | .pdf ] |
[648] | Martin Hofmann and Georg Moser. Amortised resource analysis and typed polynomial interpretations. In Typed Lambda Calculi and Applications (TLCA), volume 8560 of Lecture Notes in Computer Science, pages 272--286. Springer, July 2014. [ bib | .pdf ] |
[649] | Martin Hofmann and Mariela Pavlova. Elimination of ghost variables in program logics. In Trustworthy Global Computing, volume 4912 of Lecture Notes in Computer Science, pages 1--20. Springer, 2008. [ bib | .pdf ] |
[650] | 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 ] |
[651] | John Hogg. Islands: Aliasing protection in object-oriented languages. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 271--285, 1991. [ bib | http ] |
[652] | Benjamin Holland, Ganesh Ram Santhanam, Payas Awadhutkar, and Suresh Kothari. Statically-informed dynamic analysis tools to detect algorithmic complexity vulnerabilities. In Source Code Analysis and Manipulation (SCAM), pages 79--84, October 2016. [ bib | .pdf ] |
[653] | 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 ] |
[654] | 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, March 2000. [ bib | .ps.gz ] |
[655] | Kohei Honda and Nobuko Yoshida. A uniform type structure for secure information flow. In Principles of Programming Languages (POPL), pages 81--92, January 2002. [ bib | .ps.gz ] |
[656] | Kohei Honda and Nobuko Yoshida. A compositional logic for polymorphic higher-order functions. In Principles and Practice of Declarative Programming (PPDP), pages 191--202, August 2004. [ bib | .pdf.gz ] |
[657] | 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, 2001. [ bib | .pdf ] |
[658] | 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 ] |
[659] | John E. Hopcroft. Computer science: The emergence of a discipline. Communications of the ACM, 30(3):198--202, 1987. [ bib | http ] |
[660] | John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman. Introduction to automata theory, languages, and computation. Addison-Wesley, 2000. [ bib | .html ] |
[661] | John E. Hopcroft and Jeffrey D. Ullman. Set merging algorithms. SIAM Journal on Computing, 2(4):294--303, 1973. [ bib | http ] |
[662] | James J. Horning. What the compiler should tell the user. In Compiler Construction (CC), volume 21 of Lecture Notes in Computer Science, pages 525--548. Springer, 1974. [ bib | http ] |
[663] | R. Nigel Horspool and Michael Whitney. Even faster LR parsing. Software: Practice and Experience, 20(6):515--535, June 1990. [ bib | .pdf ] |
[664] | 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 ] |
[665] | Haruo Hosoya and Benjamin C. Pierce. Regular expression pattern matching for XML. Journal of Functional Programming, 13(6):961--1004, November 2003. [ bib | http ] |
[666] | Rodney R. Howell. On asymptotic notation with multiple variables. Technical Report 2007-4, Kansas State University, January 2008. [ bib | .pdf ] |
[667] | Rodney R. Howell. Algorithms: A top-down approach, July 2012. Draft. [ bib | http ] |
[668] | Thierry Hubert and Claude Marché. Separation analysis for deductive verification. In Heap Analysis and Verification (HAV), March 2007. [ bib | .pdf ] |
[669] | Paul Hudak, John Hughes, Simon Peyton Jones, and Philip Wadler. A history of Haskell: being lazy with class. In History of Programming Languages, June 2007. [ bib | .pdf ] |
[670] | Gérard Huet. Résolution d'équations dans des langages d'ordre 1, 2, ..., ω. PhD thesis, Université Paris 7, September 1976. [ bib ] |
[671] | Gérard Huet. The zipper. Journal of Functional Programming, 7(5):549--554, 1997. [ bib | .pdf ] |
[672] | Gérard Huet. Regular Böhm trees. Mathematical Structures in Computer Science, 8:671--680, 1998. [ bib | .pdf ] |
[673] | Brian Huffman and Christian Urban. A new foundation for Nominal Isabelle. In Interactive Theorem Proving (ITP), volume 6172 of Lecture Notes in Computer Science, pages 35--50. Springer, July 2010. [ bib | .pdf ] |
[674] | John Hughes. Why functional programming matters. Computer Journal, 32(2):98--107, 1989. [ bib | .pdf ] |
[675] | John Hughes. Generalising monads to arrows. Science of Computer Programming, 37(1--3):67--111, 2000. [ bib | .pdf ] |
[676] | John Hughes, Lars Pareto, and Amr Sabry. Proving the correctness of reactive systems using sized types. In Principles of Programming Languages (POPL), pages 410--423, January 1996. [ bib | http ] |
[677] | Graham Hutton. A tutorial on the universality and expressiveness of fold. Journal of Functional Programming, 9(4):355--372, 1999. [ bib | .pdf ] |
[678] | 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 ] |
[679] | Samin S. Ishtiaq and Peter W. O'Hearn. BI as an assertion language for mutable data structures. In Principles of Programming Languages (POPL), pages 14--26, January 2001. [ bib | .pdf ] |
[680] | Daniel Jackson and Mandana Vaziri. Finding bugs with a constraint solver. In International Symposium on Software Testing and Analysis (ISSTA), August 2000. [ bib | .pdf ] |
[681] | Bart Jacobs, Dragan Bosnacki, and Ruurd Kuipe. Modular termination verification. In European Conference on Object-Oriented Programming (ECOOP), Leibniz International Proceedings in Informatics, pages 99--1023, July 2015. [ bib | .pdf ] |
[682] | Bart Jacobs and Frank Piessens. The VeriFast program verifier. Technical Report CW-520, Department of Computer Science, Katholieke Universiteit Leuven, August 2008. [ bib | .pdf ] |
[683] | Bart Jacobs, Jan Smans, and Frank Piessens. The VeriFast program verifier: A tutorial. Unpublished, November 2017. [ bib | .pdf ] |
[684] | 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, September 1995. [ bib | .ps.gz ] |
[685] | Patrik Jansson. Functional polytypic programming. PhD thesis, Chalmers University of Technology, 2000. [ bib | .pdf ] |
[686] | C. Barry Jay. The pattern calculus. ACM Transactions on Programming Languages and Systems, 26(6):911--937, November 2004. [ bib | .pdf ] |
[687] | Clinton L. Jeffery. Merr user's guide, July 2002. [ bib | .pdf ] |
[688] | Clinton L. Jeffery. Generating LR syntax error messages from examples. ACM Transactions on Programming Languages and Systems, 25(5):631--640, 2003. [ bib | http ] |
[689] | Jonas Braband Jensen, Nick Benton, and Andrew Kennedy. High-level separation logic for low-level code. In Principles of Programming Languages (POPL), pages 301--314, January 2013. [ bib | .pdf ] |
[690] | Jonas Braband Jensen and Lars Birkedal. Fictional separation logic. In European Symposium on Programming (ESOP), volume 7211 of Lecture Notes in Computer Science, pages 377--396. Springer, March 2012. [ bib | .pdf ] |
[691] | Thomas Jensen. Inference of polymorphic and conditional strictness properties. In Principles of Programming Languages (POPL), pages 209--221. ACM Press, January 1998. [ bib | .ps ] |
[692] | 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 ] |
[693] | Thomas Jensen, Florimond Ployette, and Olivier Ridoux. Iteration schemes for fixed point computation. In International workshop on Fixed Points in Computer Science (FICS), pages 69--76, 2002. [ bib | .ps ] |
[694] | Johan Jeuring, Sean Leather, José Pedro Magalhães, and Alexey Rodriguez Yakushev. Libraries for generic programming in Haskell. In Advanced Functional Programming, volume 5832 of Lecture Notes in Computer Science, pages 165--229. Springer, May 2008. [ bib | .pdf ] |
[695] | Somesh Jha, Jens Palsberg, and Tian Zhao. Efficient type matching. In Foundations of Software Science and Computation Structures (FOSSACS), volume 2303 of Lecture Notes in Computer Science, pages 187--204. Springer, April 2002. [ bib | .pdf ] |
[696] | Ranjit Jhala, Eric Seidel, and Niki Vazou. Programming with refinement types. Unpublished, March 2017. [ bib | .pdf ] |
[697] | Limin Jia, Frances Spalding, David Walker, and Neal Glew. Certifying compilation for a language with stack allocation. In Logic in Computer Science (LICS), pages 407--416, June 2005. [ bib | .pdf ] |
[698] | Limin Jia and David Walker. ILC: A foundation for automated reasoning about pointer programs. In European Symposium on Programming (ESOP), volume 3924 of Lecture Notes in Computer Science, pages 131--145. Springer, March 2006. [ bib | .pdf ] |
[699] | 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 ] |
[700] | 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 ] |
[701] | Trevor Jim and Jens Palsberg. Type inference in systems of recursive types with subtyping. Manuscript, 1999. [ bib | .pdf ] |
[702] | Gregory F. Johnson and Janet A. Walz. A maximum-flow approach to anomaly isolation in unification-based incremental type inference. In Principles of Programming Languages (POPL), pages 44--57, January 1986. [ bib ] |
[703] | Stephen C. Johnson. Yacc: Yet another compiler-compiler. Computing Science Technical Report 32, Bell Laboratories, 1975. [ bib | .ps ] |
[704] | 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 ] |
[705] | Thomas Johnsson. Lambda lifting: Transforming programs to recursive equations. In Jean-Pierre Jouannaud, editor, Functional Programming Languages and Computer Architecture (FPCA), volume 201 of Lecture Notes in Computer Science, pages 190--203. Springer, 1985. [ bib | http ] |
[706] | Mark P. Jones. A theory of qualified types. In European Symposium on Programming (ESOP), volume 582 of Lecture Notes in Computer Science. Springer, February 1992. [ bib | .html ] |
[707] | Mark P. Jones. Dictionary-free overloading by partial evaluation. In ACM Workshop on Evaluation and Semantics-Based Program Manipulation (PEPM), June 1994. [ bib | .ps ] |
[708] | Mark P. Jones. Qualified types: Theory and practice. Cambridge University Press, November 1994. [ bib ] |
[709] | Mark P. Jones. Simplifying and improving qualified types. Technical Report YALEU/DCS/RR-1040, Yale University, June 1994. [ bib | .ps.Z ] |
[710] | Mark P. Jones. From Hindley-Milner types to first-class structures. Research Report YALEU/DCS/RR-1075, Yale University, June 1995. [ bib | .html ] |
[711] | Mark P. Jones. Using parameterized signatures to express modular structure. In Principles of Programming Languages (POPL), January 1996. [ bib | .html ] |
[712] | Mark P. Jones. Typing Haskell in Haskell. In Haskell workshop, October 1999. [ bib | http ] |
[713] | Mark P. Jones. jacc: Just another compiler compiler for Java, February 2004. [ bib | .pdf ] |
[714] | Mark P. Jones and Simon Peyton Jones. Lightweight extensible records for Haskell. In Haskell workshop, October 1999. [ bib | .ps.gz ] |
[715] | Steffen Jost, Kevin Hammond, Hans-Wolfgang Loidl, and Martin Hofmann. Static determination of quantitative resource usage for higher-order programs. In Principles of Programming Languages (POPL), pages 223--236, January 2010. [ bib | .pdf ] |
[716] | Steffen Jost, Hans-Wolfgang Loidl, Kevin Hammond, Norman Scaife, and Martin Hofmann. "carbon credits" for resource-bounded computations using amortised analysis. In Formal Methods (FM), volume 5850 of Lecture Notes in Computer Science, pages 354--369. Springer, November 2009. [ bib | .pdf ] |
[717] | 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 ] |
[718] | 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 ] |
[719] | Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David Pichardie. A formally-verified C static analyzer. In Principles of Programming Languages (POPL), pages 247--259, January 2015. [ bib | .pdf ] |
[720] | Jacques-Henri Jourdan, François Pottier, and Xavier Leroy. Validating LR(1) parsers. In European Symposium on Programming (ESOP), volume 7211 of Lecture Notes in Computer Science, pages 397--416. Springer, March 2012. [ bib | .pdf ] |
[721] | Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. RustBelt: securing the foundations of the Rust programming language. Proceedings of the ACM on Programming Languages, 2(POPL):66:1--66:34, 2018. [ bib | .pdf ] |
[722] | Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer. Higher-order ghost state. In International Conference on Functional Programming (ICFP), pages 256--269, September 2016. [ bib | .pdf ] |
[723] | Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, and Derek Dreyer. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28:e20, 2018. [ bib | .pdf ] |
[724] | Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. Iris: monoids and invariants as an orthogonal basis for concurrent reasoning. In Principles of Programming Languages (POPL), pages 637--650, January 2015. [ bib | .pdf ] |
[725] | Niels Jørgensen. Chaotic fixpoint iteration guided by dynamic dependency. In International Workshop on Static Analysis (WSA), volume 724 of Lecture Notes in Computer Science, pages 27--44. Springer, 1993. [ bib | .ps ] |
[726] | Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis. Strong logic for weak memory: Reasoning about release-acquire consistency in Iris. In European Conference on Object-Oriented Programming (ECOOP), pages 17:1--17:29, June 2017. [ bib | .pdf ] |
[727] | Jonas Kaiser, Tobias Tebbi, and Gert Smolka. Equivalence of System F and λ2 in Coq based on context morphism lemmas. In Certified Programs and Proofs (CPP), pages 222--234, January 2017. [ bib | .pdf ] |
[728] | 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 ] |
[729] | John B. Kam and Jeffrey D. Ullman. Monotone data flow analysis frameworks. Acta Informatica, 7(3):305--317, September 1977. [ bib | http ] |
[730] | Ohad Kammar, Sam Lindley, and Nicolas Oury. Handlers in action. In International Conference on Functional Programming (ICFP), pages 145--158, September 2013. [ bib | .pdf ] |
[731] | Ohad Kammar and Matija Pretnar. No value restriction is needed for algebraic effects and handlers. Journal of Functional Programming, 27:e7, 2017. [ bib | .pdf ] |
[732] | Johannes Kanig. Specification and proof of higher-order programs. PhD thesis, Université Paris-Sud, November 2010. [ bib | .pdf ] |
[733] | E. Kantorowitz and H. Laor. Automatic generation of useful syntax error messages. Software: Practice and Experience, 16(7):627--640, 1986. [ bib | http ] |
[734] | Haim Kaplan, Nira Shafrir, and Robert E. Tarjan. Union-find with deletions. In Symposium on Discrete Algorithms (SODA), pages 19--28, January 2002. [ bib | http ] |
[735] | Haim Kaplan and Robert E. Tarjan. Purely functional, real-time deques with catenation. Journal of the ACM, 46(5):577--603, 1999. [ bib | .ps ] |
[736] | Deepak Kapur and Hantao Zhang. An overview of Rewrite Rule Laboratory (RRL). J. Comput. Appl. Math., 29(2):91--114, 1995. [ bib | .ps.gz ] |
[737] | Aleksandr Karbyshev. Monadic parametricity of second-order functionals. PhD thesis, Technische Universität München, 2013. [ bib | http ] |
[738] | Yugo Kashiwagi and David S. Wise. Graph algorithms in a lazy functional programming language. Technical Report 330, Indiana University, April 1991. [ bib | .pdf ] |
[739] | Ioannis T. Kassios. Dynamic frames: Support for framing, dependencies and sharing without restrictions. In Formal Methods (FM), volume 4085 of Lecture Notes in Computer Science, pages 268--283. Springer, August 2006. [ bib | .pdf ] |
[740] | Misa Keinänen. Techniques for solving Boolean equation systems. PhD thesis, Helsinki University of Technology, 2006. Research Report HUT-TCS-A105. [ bib | .pdf ] |
[741] | Torbjörn Keisu. Finite and rational tree constraints. Bulletin of the IGPL, 2(2):167--204, 1994. [ bib | .ps.gz ] |
[742] | Torbjörn Keisu. Tree constraints. PhD thesis, The Royal Institute of Technology (KTH), May 1994. [ bib | .ps.gz ] |
[743] | Andrew Kennedy. Dimension types. In European Symposium on Programming (ESOP), volume 788 of Lecture Notes in Computer Science. Springer, 1994. [ bib | .pdf ] |
[744] | Andrew Kennedy. Type inference and equational theories. Technical Report LIX/RR/96/09, École Polytechnique, September 1996. [ bib ] |
[745] | Andrew Kennedy. Compiling with continuations, continued. In International Conference on Functional Programming (ICFP), pages 177--190, September 2007. [ bib | .pdf ] |
[746] | Ken W. Kennedy. Node listings applied to data flow analysis. In Principles of Programming Languages (POPL), pages 10--21, January 1975. [ bib | http ] |
[747] | 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 ] |
[748] | Brian W. Kernighan and Dennis Ritchie. The C programming language, second edition. Prentice Hall, 1988. [ bib ] |
[749] | Steven Keuchel and Tom Schrijvers. InBound: simple yet powerful specification of syntax with binders. Unpublished, February 2015. [ bib | .pdf ] |
[750] | Steven Keuchel, Stephanie Weirich, and Tom Schrijvers. Needle & knot: Binder boilerplate tied up. In European Symposium on Programming (ESOP), volume 9632 of Lecture Notes in Computer Science, pages 419--445. Springer, April 2016. [ bib | .pdf ] |
[751] | 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 ] |
[752] | 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, May 1990. [ bib | http ] |
[753] | 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 ] |
[754] | Richard B. Kieburtz. Taming effects with monadic typing. In International Conference on Functional Programming (ICFP), pages 51--62, 1998. [ bib | http ] |
[755] | Richard B. Kieburtz. P-logic: Property verification for Haskell programs. Draft, August 2002. [ bib | .pdf ] |
[756] | Gary A. Kildall. A unified approach to global program optimization. In Principles of Programming Languages (POPL), pages 194--206, October 1973. [ bib | http ] |
[757] | Ik-Soon Kim, Kwangkeun Yi, and Cristiano Calcagno. A polymorphic modal type system for Lisp-like multi-staged languages. In Principles of Programming Languages (POPL), pages 257--268, 2006. [ bib | .pdf ] |
[758] | David King and Philip Wadler. Combining monads. In Workshop on Functional Programming. Springer, 1992. [ bib | .ps.gz ] |
[759] | Oleg Kiselyov and Chung-chieh Shan. A substructural type system for delimited continuations. In Typed Lambda Calculi and Applications (TLCA), volume 4583 of Lecture Notes in Computer Science, pages 223--239. Springer, June 2007. [ bib | .pdf ] |
[760] | Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: formal verification of an operating-system kernel. Communications of the ACM, 53(6):107--115, 2010. [ bib | .pdf ] |
[761] | Paul Klint, Ralf Lämmel, and Chris Verhoef. Toward an engineering discipline for grammarware. ACM Transactions on Software Engineering and Methodology, 14(3):331--380, 2005. [ bib | .pdf ] |
[762] | Johannes Kloos, Rupak Majumdar, and Viktor Vafeiadis. Asynchronous liquid separation types. In European Conference on Object-Oriented Programming (ECOOP), pages 396--420, July 2015. [ bib | .pdf ] |
[763] | Edward Kmett. Bound. Blog post, November 2014. [ bib | http ] |
[764] | Kevin Knight. Unification: a multidisciplinary survey. ACM Computing Surveys, 21(1):93--124, March 1989. [ bib | http ] |
[765] | Donald E. Knuth. On the translation of languages from left to right. Information & Control, 8(6):607--639, December 1965. [ bib | http ] |
[766] | Donald E. Knuth. A generalization of Dijkstra's algorithm. Information Processing Letters, 6(1):1--5, February 1977. [ bib ] |
[767] | Naoki Kobayashi. A partially deadlock-free typed process calculus. ACM Transactions on Programming Languages and Systems, 20(2):436--482, March 1998. [ bib | http ] |
[768] | 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 ] |
[769] | 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 ] |
[770] | 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, August 2000. [ bib | .ps.gz ] |
[771] | 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 ] |
[772] | 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 ] |
[773] | Eugene E. Kohlbecker and Mitchell Wand. Macro-by-example: Deriving syntactic transformations from their specifications. In Principles of Programming Languages (POPL), pages 77--84, January 1987. [ bib | http ] |
[774] | Gabriël Konat, Lennart Kats, Guido Wachsmuth, and Eelco Visser. Declarative name binding and scope rules. In Software Language Engineering, volume 7745 of Lecture Notes in Computer Science, pages 311--331. Springer, September 2013. [ bib | .pdf ] |
[775] | Adam Koprowski and Henri Binsztok. TRX: A formally verified parser interpreter. In European Symposium on Programming (ESOP), volume 6012 of Lecture Notes in Computer Science, pages 345--365. Springer, March 2010. [ bib | .pdf ] |
[776] | Adam Koprowski and Henri Binsztok. TRX: A formally verified parser interpreter. Logical Methods in Computer Science, 7(2), 2011. [ bib | http ] |
[777] | Larry Koved, Marco Pistoia, and Aaron Kershenbaum. Access rights analysis for Java. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 359--372, November 2002. [ bib | .pdf ] |
[778] | Dexter Kozen, Jens Palsberg, and Michael I. Schwartzbach. Efficient recursive subtyping. Mathematical Structures in Computer Science, 5(1):113--125, 1995. [ bib | .pdf ] |
[779] | Dexter C. Kozen. The design and analysis of algorithms. Texts and Monographs in Computer Science. Springer, 1992. [ bib | .pdf ] |
[780] | Robbert Krebbers, Ralf Jung, Aleš Bizjak, Jacques-Henri Jourdan, Derek Dreyer, and Lars Birkedal. The essence of higher-order concurrent separation logic. In European Symposium on Programming (ESOP), volume 10201 of Lecture Notes in Computer Science, pages 696--723. Springer, April 2017. [ bib | .pdf ] |
[781] | Robert Krebbers, Amin Timany, and Lars Birkedal. Interactive proofs in higher-order concurrent separation logic. In Principles of Programming Languages (POPL), January 2017. [ bib | .pdf ] |
[782] | 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, September 1999. [ bib | .ps ] |
[783] | Neelakantan R. Krishnaswami. Verifying higher-order imperative programs with higher-order separation logic. PhD thesis, School of Computer Science, Carnegie Mellon University, 2012. [ bib | .pdf ] |
[784] | Neelakantan R. Krishnaswami, Jonathan Aldrich, Lars Birkedal, Kasper Svendsen, and Alexandre Buisse. Design patterns in separation logic. In Types in Language Design and Implementation (TLDI), pages 105--116, January 2009. [ bib | .pdf ] |
[785] | Neelakantan R. Krishnaswami, Aaron Turon, Derek Dreyer, and Deepak Garg. Superficially substructural types. In International Conference on Functional Programming (ICFP), pages 41--54, September 2012. [ bib | .pdf ] |
[786] | Daniel Kroening and Ofer Strichman. Decision procedures -- an algorithmic point of view. Springer, 2008. [ bib | http ] |
[787] | George Kuan and David MacQueen. Efficient type inference using ranked type variables. In ACM Workshop on ML, pages 3--14, October 2007. [ bib | .pdf ] |
[788] | Viktor Kuncak and Martin Rinard. On the theory of structural subtyping. Technical Report 879, MIT Laboratory for Computer Science, January 2003. [ bib | .ps ] |
[789] | Viktor Kuncak and Martin Rinard. Structural subtyping of non-recursive types is decidable. In Logic in Computer Science (LICS), June 2003. [ bib | .pdf ] |
[790] | 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 ] |
[791] | Ralf Lämmel and Simon Peyton Jones. Scrap your boilerplate: a practical design pattern for generic programming. In Types in Language Design and Implementation (TLDI), pages 26--37, January 2003. [ bib | .pdf ] |
[792] | Ralf Lämmel and Simon Peyton Jones. Scrap more boilerplate: reflection, zips, and generalised casts. In International Conference on Functional Programming (ICFP), pages 244--255, September 2004. [ bib | http ] |
[793] | Ralf Lämmel and Simon Peyton Jones. Scrap your boilerplate with class: extensible generic functions. In International Conference on Functional Programming (ICFP), pages 204--215, September 2005. [ bib | .pdf ] |
[794] | Peter Lammich. Automatic data refinement. In Interactive Theorem Proving (ITP), volume 7998 of Lecture Notes in Computer Science, pages 84--99. Springer, July 2013. [ bib | .pdf ] |
[795] | Peter Lammich. Verified efficient implementation of Gabow's strongly connected component algorithm. In Interactive Theorem Proving (ITP), volume 8558 of Lecture Notes in Computer Science, pages 325--340. Springer, July 2014. [ bib | .pdf ] |
[796] | Peter Lammich. Refinement to Imperative/HOL. In Interactive Theorem Proving (ITP), volume 9236 of Lecture Notes in Computer Science, pages 253--269. Springer, August 2015. [ bib | .pdf ] |
[797] | Peter Lammich. Refinement based verification of imperative data structures. In Certified Programs and Proofs (CPP), pages 27--36, January 2016. [ bib | .pdf ] |
[798] | Peter Lammich and Andreas Lochbihler. The Isabelle collections framework. In Interactive Theorem Proving (ITP), volume 6172 of Lecture Notes in Computer Science, pages 339--354. Springer, July 2010. [ bib | .pdf ] |
[799] | Peter Lammich and Rene Meis. A separation logic framework for Imperative HOL. Archive of Formal Proofs, 2012. [ bib | http ] |
[800] | Peter Lammich and René Neumann. A framework for verifying depth-first search algorithms. In Certified Programs and Proofs (CPP), pages 137--146, January 2015. [ bib | .pdf ] |
[801] | Butler W. Lampson. A note on the confinement problem. Communications of the ACM, 16(10):613--615, October 1973. [ bib | .html ] |
[802] | Peter J. Landin. The mechanical evaluation of expressions. Computer Journal, 6(4):308--320, January 1964. [ bib ] |
[803] | 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 ] |
[804] | James Richard Larus. Restructuring symbolic programs for concurrent execution on multiprocessors. PhD thesis, EECS Department, University of California, Berkeley, May 1989. Technical Report UCB/CSD-89-502. [ bib | .pdf ] |
[805] | Soren B. Lassen. Bisimulation in untyped lambda calculus: Böhm trees and bisimulation up to context. In Mathematical Foundations of Programming Semantics, volume 20 of Electronic Notes in Theoretical Computer Science, pages 346--374. Elsevier Science, April 1999. [ bib | .ps ] |
[806] | Soren B. Lassen. Head normal form bisimulation for pairs and the λμ-calculus. In Logic in Computer Science (LICS), pages 297--306, August 2006. [ bib | .pdf ] |
[807] | 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 ] |
[808] | Jean-Louis Lassez, V. L. Nguyen, and Liz Sonenberg. Fixed point theorems and semantics: a folk tale. Information Processing Letters, 14(3):112--116, May 1982. [ bib | http ] |
[809] | 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 ] |
[810] | John Launchbury and Simon Peyton Jones. State in Haskell. LISP and Symbolic Computation, 8(4):293--341, 1995. [ bib | http ] |
[811] | Vincent Laviron, Bor-Yuh Evan Chang, and Xavier Rival. Separating shape graphs. In European Symposium on Programming (ESOP), volume 6012 of Lecture Notes in Computer Science, pages 387--406. Springer, March 2010. [ bib | .pdf ] |
[812] | Julia L. Lawall and Olivier Danvy. Separating stages in the continuation-passing style transformation. In Principles of Programming Languages (POPL), pages 124--136, January 1993. [ bib | .ps.gz ] |
[813] | Didier Le Botlan and Didier Rémy. MLF: Raising ML to the power of system F. In International Conference on Functional Programming (ICFP), pages 27--38, August 2003. [ bib | .pdf ] |
[814] | Baudouin Le Charlier and Pascal Van Hentenryck. A universal top-down fixpoint algorithm. Technical Report CS-92-25, Brown University, May 1992. [ bib | .ps.gz ] |
[815] | Fabrice Le Fessant and Luc Maranget. Optimizing pattern matching. In International Conference on Functional Programming (ICFP), 2001. [ bib | .ps.gz ] |
[816] | Daniel Le Métayer. ACE: an automatic complexity evaluator. ACM Transactions on Programming Languages and Systems, 10(2):248--266, 1988. [ bib | http ] |
[817] | Christopher League, Zhong Shao, and Valery Trifonov. Representing Java classes in a typed intermediate language. In International Conference on Functional Programming (ICFP), pages 183--196, September 1999. [ bib | .html ] |
[818] | 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 ] |
[819] | Christopher League, Zhong Shao, and Valery Trifonov. Precision in practice: a type-preserving Java compiler. In Compiler Construction (CC), volume 2622 of Lecture Notes in Computer Science, pages 106--120. Springer, April 2003. [ bib | .html ] |
[820] | Gary T. Leavens and Albert L. Baker. Enhancing the pre- and postcondition technique for more expressive specifications. In Formal Methods (FM), volume 1709 of Lecture Notes in Computer Science, pages 1087--1106. Springer, January 1999. [ bib | http ] |
[821] | Gary T. Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, Peter Müller, Joseph Kiniry, Patrice Chalin, and Daniel M. Zimmerman. JML reference manual, May 2008. [ bib | .pdf ] |
[822] | Sylvain Lebresne. A system F with call-by-name exceptions. In International Colloquium on Automata, Languages and Programming, volume 5126 of Lecture Notes in Computer Science, pages 323--335. Springer, June 2008. [ bib | .pdf ] |
[823] | Gyesik Lee, Bruno C. d. S. Oliveira, Sungkeun Cho, and Kwangkeun Yi. GMeta: A generic formal metatheory framework for first-order representations. In European Symposium on Programming (ESOP), volume 7211 of Lecture Notes in Computer Science, pages 436--455. Springer, April 2012. [ bib | .pdf ] |
[824] | 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 ] |
[825] | Daan Leijen. Koka: Programming with row polymorphic effect types. In Workshop on Mathematically Structured Functional Programming (MSFP), volume 153, pages 100--126, April 2014. [ bib | .pdf ] |
[826] | Daan Leijen. Algebraic effects for functional programming. Technical Report MSR-TR-2016-29, Microsoft Research, August 2016. [ bib | http ] |
[827] | K. Rustan M. Leino. Efficient weakest preconditions. Information Processing Letters, 93(6):281--288, 2005. [ bib | .pdf ] |
[828] | K. Rustan M. Leino. Dafny: An automatic program verifier for functional correctness. In Logic for Programming Artificial Intelligence and Reasoning (LPAR), volume 6355 of Lecture Notes in Computer Science, pages 348--370. Springer, April 2010. [ bib | .pdf ] |
[829] | K. Rustan M. Leino and Michal Moskal. VACID-0: Verification of ample correctness of invariants of data-structures, edition 0. Manuscript KRML 209, July 2010. [ bib | .pdf ] |
[830] | K. Rustan M. Leino and Peter Müller. A basis for verifying multi-threaded programs. In European Symposium on Programming (ESOP), volume 5502 of Lecture Notes in Computer Science, pages 378--393. Springer, March 2009. [ bib | .pdf ] |
[831] | K. Rustan M. Leino, Peter Müller, and Jan Smans. Verification of concurrent programs with Chalice. In Foundations of Security Analysis and Design, volume 5705 of Lecture Notes in Computer Science, pages 195--222. Springer, 2009. [ bib | .pdf ] |
[832] | K. Rustan M. Leino, Peter Müller, and Jan Smans. Deadlock-free channels and locks. In European Symposium on Programming (ESOP), volume 6012 of Lecture Notes in Computer Science, pages 407--426. Springer, March 2010. [ bib | .pdf ] |
[833] | 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 ] |
[834] | K. Rustan M. Leino and Wolfram Schulte. Using history invariants to verify observers. In European Symposium on Programming (ESOP), volume 4421 of Lecture Notes in Computer Science, pages 80--94. Springer, 2007. [ bib | .pdf ] |
[835] | Caroline Lemieux, Rohan Padhye, Koushik Sen, and Dawn Song. PerfFuzz: Automatically generating pathological inputs. In International Symposium on Software Testing and Analysis (ISSTA), pages 254--265, 2018. [ bib | .pdf ] |
[836] | Xavier Leroy. Polymorphic typing of an algorithmic language. Research Report 1778, INRIA, October 1992. [ bib | .ps.gz ] |
[837] | Xavier Leroy. Typage polymorphe d'un langage algorithmique. PhD thesis, Université Paris 7, June 1992. [ bib | .ps.gz ] |
[838] | Xavier Leroy. A modular module system. Journal of Functional Programming, 10(3):269--303, 2000. [ bib | .pdf ] |
[839] | Xavier Leroy. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In Principles of Programming Languages (POPL), pages 42--54, January 2006. [ bib | .pdf ] |
[840] | Xavier Leroy. The CompCert C compiler. http://compcert.inria.fr/, 2015. [ bib ] |
[841] | Xavier Leroy, Damien Doligez, Alain Frisch, Jacques Garrigue, Didier Rémy, and Jérôme Vouillon. The OCaml system: documentation and user's manual, 2019. [ bib | http ] |
[842] | Xavier Leroy, Damien Doligez, Jacques Garrigue, Didier Rémy, and Jérôme Vouillon. The Objective Caml system, October 2005. [ bib | http ] |
[843] | Xavier Leroy, Damien Doligez, Michel Mauny, and Pierre Weis. The Caml Light system, release 0.75, 2002. [ bib | http ] |
[844] | Xavier Leroy and François Pottier. Notes du cours de DEA « typage et programmation », December 2002. [ bib | .ps.gz ] |
[845] | Stéphane Lescuyer. First-class containers in Coq. Studia Informatica Universalis, 9(1):87--127, 2011. [ bib | .pdf ] |
[846] | 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 ] |
[847] | Thomas Letan, Yann Régis-Gianas, Pierre Chifflier, and Guillaume Hiet. Modular verification of programs with effects and effect handlers in Coq. In Formal Methods (FM), volume 10951 of Lecture Notes in Computer Science, pages 338--354. Springer, July 2018. [ bib | http ] |
[848] | Pierre Letouzey. Programmation fonctionnelle certifiée -- l'extraction de programmes dans l'assistant Coq. PhD thesis, Université Paris 11, July 2004. [ bib | .ps.gz ] |
[849] | Paul Blain Levy. Possible world semantics for general storage in call-by-value. In Computer Science Logic, volume 2471 of Lecture Notes in Computer Science. Springer, 2002. [ bib | .ps ] |
[850] | Jeffrey Lewis, Mark Shields, Erik Meijer, and John Launchbury. Implicit parameters: Dynamic scoping with static types. In Principles of Programming Languages (POPL), pages 108--118, January 2000. [ bib | .ps ] |
[851] | Ruy Ley-Wild and Aleksandar Nanevski. Subjective auxiliary state for coarse-grained concurrency. In Principles of Programming Languages (POPL), pages 561--574, January 2013. [ bib | .pdf ] |
[852] | Daniel R. Licata and Robert Harper. A universe of binding and computation. In International Conference on Functional Programming (ICFP), pages 123--134, September 2009. [ bib | .pdf ] |
[853] | Daniel R. Licata, Noam Zeilberger, and Robert Harper. Focusing on binding and computation. In Logic in Computer Science (LICS), pages 241--252, June 2008. [ bib | .pdf ] |
[854] | Daniel R. Licata, Noam Zeilberger, and Robert Harper. Focusing on binding and computation. Technical Report CMU-CS-08-101, Carnegie Mellon University, February 2008. [ bib | .pdf ] |
[855] | Sam Lindley, Conor McBride, and Craig McLaughlin. Do be do be do. In Principles of Programming Languages (POPL), January 2017. [ bib | .pdf ] |
[856] | Nathan Linger and Tim Sheard. Programming with static invariants in Ωmega. Unpublished, September 2004. [ bib | .ps ] |
[857] | Barbara Liskov and John V. Guttag. Program development in Java -- abstraction, specification, and object-oriented design. Addison-Wesley, 2001. [ bib | http ] |
[858] | Barbara Liskov and Jeannette M. Wing. A behavioral notion of subtyping. ACM Transactions on Programming Languages and Systems, 16(6):1811--1841, 1994. [ bib | .pdf ] |
[859] | Xinxin Liu and Scott A. Smolka. Simple linear-time algorithms for minimal fixed points. In International Colloquium on Automata, Languages and Programming, volume 1443 of Lecture Notes in Computer Science, pages 53--66. Springer, July 1998. [ bib | http ] |
[860] | Andreas Lochbihler. Light-weight containers for Isabelle: efficient, extensible, nestable. In Interactive Theorem Proving (ITP), volume 7998 of Lecture Notes in Computer Science, pages 116--132. Springer, July 2013. [ bib | .pdf ] |
[861] | John Longley. When is a functional program not a functional program? In International Conference on Functional Programming (ICFP), pages 1--7, September 1999. [ bib | http ] |
[862] | John Longley and Randy Pollack. Reasoning about CBV functional programs in Isabelle/HOL. In Theorem Proving in Higher Order Logics (TPHOLs), volume 3223 of Lecture Notes in Computer Science, pages 201--216. Springer, September 2004. [ bib | .pdf ] |
[863] | John M. Lucassen and David K. Gifford. Polymorphic effect systems. In Principles of Programming Languages (POPL), pages 47--57, January 1988. [ bib | .pdf ] |
[864] | Ralf Lämmel and Simon Peyton Jones. Scrap your boilerplate with class: extensible generic functions. Submitted, April 2005. [ bib | .ps ] |
[865] | Ralf Lämmel, Joost Visser, and Jan Kort. Dealing with large bananas. In Workshop on Generic Programming, pages 46--59, July 2000. [ bib | .ps ] |
[866] | Kenneth MacKenzie and Nicholas Wolverson. Camelot and Grail: resource-aware functional programming for the JVM. In Trends in Functional Programming (TFP), volume 4, pages 29--46, September 2003. [ bib | .ps ] |
[867] | 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 ] |
[868] | Angelika Mader. Verification of modal properties using Boolean equation systems. PhD thesis, Technische Universität München, 1997. [ bib | .pdf ] |
[869] | Ravichandhran Madhavan, Sumith Kulal, and Viktor Kuncak. Contract-based resource verification for higher-order functions with memoization. In Principles of Programming Languages (POPL), pages 330--343, January 2017. [ bib | .pdf ] |
[870] | Magnus Madsen, Ming-Ho Yee, and Ondrej Lhoták. From Datalog to Flix: a declarative language for fixed points on lattices. In Programming Language Design and Implementation (PLDI), pages 194--208, June 2016. [ bib | .pdf ] |
[871] | Toshiyuki Maeda, Haruki Sato, and Akinori Yonezawa. Extended alias type system using separating implication. In Types in Language Design and Implementation (TLDI), pages 29--42, January 2011. [ bib | http ] |
[872] | Michael J. Maher. Complete axiomatizations of the algebras of finite, rational and infinite trees. In Logic in Computer Science (LICS), pages 348--357, July 1988. [ bib ] |
[873] | Harry G. Mairson. Deciding ML typability is complete for deterministic exponential time. In Principles of Programming Languages (POPL), pages 382--401, 1990. [ bib | http ] |
[874] | 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 ] |
[875] | 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 ] |
[876] | Filip Marić. Formalization and implementation of modern SAT solvers. Journal of Automated Reasoning, 43:81--119, 2009. [ bib | .pdf ] |
[877] | Filip Marić. Formal verification of a modern SAT solver. Unpublished, January 2010. [ bib | .pdf ] |
[878] | Simon Marlow and Andy Gill. Happy: the parser generator for Haskell, April 2004. [ bib | http ] |
[879] | Simon Marlow and Philip Wadler. A practical subtyping system for Erlang. In International Conference on Functional Programming (ICFP), pages 136--149, June 1997. [ bib ] |
[880] | Kim Marriott and Martin Odersky. Negative Boolean constraints. Technical Report 94/203, Monash University, August 1994. [ bib | .ps.gz ] |
[881] | Alberto Martelli and Ugo Montanari. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems, 4(2):258--282, April 1982. [ bib | http ] |
[882] | Guido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Catalin Hritcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, and Nikhil Swamy. Meta-F^{}: Proof automation with SMT, tactics, and metaprograms. In European Symposium on Programming (ESOP), volume 11423 of Lecture Notes in Computer Science, pages 30--59. Springer, April 2019. [ bib | .pdf ] |
[883] | Radu Mateescu and Mihaela Sighireanu. Efficient on-the-fly model-checking for regular alternation-free mu-calculus. Science of Computer Programming, 46(3):255--281, 2003. [ bib | .pdf ] |
[884] | Nicholas D. Matsakis and Felix S. Klock,II. The Rust language. In ACM SIGAda Annual Conference on High Integrity Language Technology (HILT), pages 103--104, 2014. [ bib | http ] |
[885] | Michel Mauny and François Pottier. An implementation of Caml Light with existential types. Technical Report 2183, INRIA, 1993. [ bib | .ps.gz ] |
[886] | Karl Mazurak, Jianzhou Zhao, and Steve Zdancewic. Lightweight linear types in system F^{o}. In Types in Language Design and Implementation (TLDI), pages 77--88, January 2010. [ bib | .pdf ] |
[887] | 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, September 1998. [ bib | .ps ] |
[888] | David McAllester. On the complexity analysis of static analyses. Journal of the ACM, 49(4):512--537, July 2002. [ bib | http ] |
[889] | 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, June 2003. [ bib | .ps ] |
[890] | Conor McBride. The derivative of a regular type is its type of one-hole contexts. Unpublished. [ bib | .pdf ] |
[891] | Conor McBride. First-order unification by structural recursion. Journal of Functional Programming, 13(6):1061--1075, 2003. [ bib | .ps.gz ] |
[892] | Conor McBride and James McKinna. I am not a number: I am a free variable. In Haskell workshop, September 2004. [ bib | .pdf ] |
[893] | Conor McBride and Ross Paterson. Applicative programming with effects. Journal of Functional Programming, 18(1):1--13, 2008. [ bib | .pdf ] |
[894] | Jay A. McCarthy, Burke Fetscher, Max S. New, Daniel Feltey, and Robert Bruce Findler. A Coq library for internal verification of running-times. In Functional and Logic Programming, volume 9613 of Lecture Notes in Computer Science, pages 144--162. Springer, March 2016. [ bib | .pdf ] |
[895] | James McKinna and Randy Pollack. Pure type systems formalized. In Typed Lambda Calculi and Applications (TLCA), number 664 in Lecture Notes in Computer Science, pages 289--305. Springer, March 1993. [ bib | .ps.gz ] |
[896] | James McKinna and Randy Pollack. Some lambda calculus and type theory formalized. Journal of Automated Reasoning, 23(3--4):373--409, 1999. [ bib ] |
[897] | 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 ] |
[898] | John McLean. Security models. In John Marciniak, editor, Encyclopedia of Software Engineering. John Wiley & Sons, 1994. [ bib | .ps ] |
[899] | 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, 1995. [ bib | .ps ] |
[900] | Farhad Mehta and Tobias Nipkow. Proving pointer programs in higher-order logic. Information and Computation, 199(1--2):200--227, 2005. [ bib | .ps.gz ] |
[901] | Thomas F. Melham. The HOL logic extended with quantification over type variables. Formal Methods in System Design, 3(1--2):7--24, August 1993. [ bib | .pdf ] |
[902] | 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 ] |
[903] | Stephan Merz. Model checking: A tutorial overview. In Fourth Summer School on Modeling and Verification of Parallel Processes, volume 2067 of Lecture Notes in Computer Science, pages 3--38. Springer, 2001. [ bib | .pdf ] |
[904] | Stephan Merz. An introduction to model checking. In N. Navet and S. Merz, editors, Modeling and Verification of Real-Time Systems: Formalisms and Software Tools, pages 77--109. ISTE Publishing, 2008. [ bib | .pdf ] |
[905] | Albert R. Meyer and Mitchell Wand. Continuation semantics in typed lambda-calculi. In Logics of Programs, volume 193 of Lecture Notes in Computer Science, pages 219--224. Springer, June 1985. [ bib | .ps ] |
[906] | Dale Miller. An extension to ML to handle bound variables in data structures. In Logical Frameworks BRA Workshop, May 1990. [ bib | .pdf ] |
[907] | Dale Miller. Unification under a mixed prefix. Journal of Symbolic Computation, 14(4):321--358, 1992. [ bib | .pdf ] |
[908] | Dale Miller. Abstract syntax for variable binders: An overview. In Computational Logic, volume 1861 of Lecture Notes in Computer Science, pages 239--253. Springer, July 2000. [ bib | .pdf ] |
[909] | Todd Millstein and Craig Chambers. Modular statically typed multimethods. In European Conference on Object-Oriented Programming (ECOOP), volume 1628 of Lecture Notes in Computer Science, pages 279--303. Springer, June 1999. [ bib | .ps ] |
[910] | Todd Millstein and Craig Chambers. Modular statically typed multimethods. Information and Computation, 175(1):76--118, May 2002. [ bib | .ps ] |
[911] | 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 ] |
[912] | 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 ] |
[913] | Robin Milner. Models of LCF. Technical Report CS-TR-73-332, Stanford University, Department of Computer Science, January 1973. [ bib | .pdf ] |
[914] | Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17(3):348--375, December 1978. [ bib | http ] |
[915] | 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 ] |
[916] | Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, part 2. Technical Report ECS-LFCS-89-86, Laboratory for Foundations of Computer Science, School of Informatics at the University of Edinburgh, 1989. [ bib | .ps ] |
[917] | 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, July 1992. [ bib | .ps.gz ] |
[918] | Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The definition of Standard ML -- revised. MIT Press, May 1997. [ bib ] |
[919] | Yasuhiko Minamide. A functional representation of data structures with a hole. In Principles of Programming Languages (POPL), pages 75--84, January 1998. [ bib | .pdf ] |
[920] | Yasuhiko Minamide, Greg Morrisett, and Robert Harper. Typed closure conversion. In Principles of Programming Languages (POPL), pages 271--283, January 1996. [ bib | .pdf ] |
[921] | Yasuhiko Minamide and Koji Okuma. Verifying CPS transformations in Isabelle/HOL. In ACM Workshop on Mechanized Reasoning about Languages with Variable Binding, 2003. [ bib | http ] |
[922] | Yaron Minsky, Anil Madhavapeddy, and Jason Hickey. Real world OCaml: Functional programming for the masses. O'Reilly, 2013. [ bib | http ] |
[923] | David G. Mitchell. A SAT solver primer. Bulletin of the EATCS, 85:112--133, February 2005. [ bib | .pdf ] |
[924] | John C. Mitchell. Coercion and type inference. In Principles of Programming Languages (POPL), pages 175--185, January 1984. [ bib | http ] |
[925] | John C. Mitchell. Representation independence and data abstraction. In Principles of Programming Languages (POPL), pages 263--276, 1986. [ bib | http ] |
[926] | John C. Mitchell. Polymorphic type inference and containment. Information and Computation, 76(2--3):211--249, 1988. [ bib | http ] |
[927] | John C. Mitchell. Type inference with simple subtypes. Journal of Functional Programming, 1(3):245--286, July 1991. [ bib ] |
[928] | John C. Mitchell. Foundations for programming languages. MIT Press, 1996. [ bib ] |
[929] | John C. Mitchell and Gordon D. Plotkin. Abstract types have existential type. ACM Transactions on Programming Languages and Systems, 10(3):470--502, 1988. [ bib | .pdf ] |
[930] | 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 ] |
[931] | Eugenio Moggi. An abstract view of programming languages. Technical Report ECS-LFCS-90-113, University of Edinburgh, June 1989. [ bib | .ps.gz ] |
[932] | Eugenio Moggi. Computational λ-calculus and monads. In Logic in Computer Science (LICS), pages 14--23, June 1989. [ bib | .ps.gz ] |
[933] | Eugenio Moggi. Notions of computation and monads. Information and Computation, 93(1), 1991. [ bib | .pdf ] |
[934] | Eugenio Moggi and Amr Sabry. An abstract monadic semantics for value recursion. Informatique théorique et applications, 38(4):377--400, 2004. [ bib | .pdf ] |
[935] | Anders Møller and Michael I. Schwartzbach. The pointer assertion logic engine. In Programming Language Design and Implementation (PLDI), pages 221--231, June 2001. [ bib | .pdf ] |
[936] | Stefan Monnier. Statically tracking state with typed regions. Unpublished, May 2008. [ bib | .pdf ] |
[937] | Benoît Montagu and Didier Rémy. Modeling abstract types in modules with open existential types. In Principles of Programming Languages (POPL), pages 63--74, January 2009. [ bib | .pdf ] |
[938] | Andrew Moran and David Sands. Improvement in a lazy context: An operational theory for call-by-need. In Principles of Programming Languages (POPL), pages 43--56, January 1999. [ bib | .pdf ] |
[939] | 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 ] |
[940] | Greg Morrisett and Robert Harper. Typed closure conversion for recursively-defined functions (extended abstract). In Higher Order Operational Techniques in Semantics (HOOTS), volume 10 of Electronic Notes in Theoretical Computer Science. Elsevier Science, 1998. [ bib | .ps ] |
[941] | 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 ] |
[942] | 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 ] |
[943] | Peter D. Mosses. Modular structural operational semantics. Journal of Logic and Algebraic Programming, 60--61:195--228, 2004. [ bib | .pdf ] |
[944] | Rashmi Mudduluru and Murali Krishna Ramanathan. Efficient flow profiling for detecting performance bugs. In International Symposium on Software Testing and Analysis (ISSTA), pages 413--424, 2016. [ bib | .pdf ] |
[945] | Gilles Muller, Renaud Marlet, Eugen-Nicolae Volanschi, Charles Consel, Calton Pu, and Ashvin Goel. Fast, optimized Sun RPC using automatic program specialization. In International Conference on Distributed Computing Systems (CDCS), pages 240--249, May 1998. [ bib | .pdf ] |
[946] | 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 ] |
[947] | Martin Müller. Notes on HM(X). Unpublished, August 1998. [ bib | .ps.gz ] |
[948] | 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 ] |
[949] | 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, December 1998. [ bib | .ps ] |
[950] | 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 ] |
[951] | Peter Müller and Arnd Poetzsch-Heffter. Universes: A type system for alias and dependency control. Technical Report 279, Fernuniversität Hagen, 2001. [ bib | .pdf ] |
[952] | Peter Müller and Arsenii Rudich. Ownership transfer in universe types. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 461--478, October 2007. [ bib | http ] |
[953] | Peter Müller, Malte Schwerhoff, and Alexander J. Summers. Automatic verification of iterated separating conjunctions using symbolic execution. In Computer Aided Verification (CAV), volume 9779 of Lecture Notes in Computer Science, pages 405--425. Springer, July 2016. [ bib | http ] |
[954] | Peter Müller, Malte Schwerhoff, and Alexander J. Summers. Viper: A verification infrastructure for permission-based reasoning. In Dependable Software Systems Engineering, pages 104--125. 2017. [ bib | http ] |
[955] | 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, April 1984. [ bib | http ] |
[956] | Andrew C. Myers. JFlow: practical mostly-static information flow control. In Principles of Programming Languages (POPL), pages 228--241, January 1999. [ bib | .ps.gz ] |
[957] | 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 ] |
[958] | 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 ] |
[959] | 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 ] |
[960] | 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 ] |
[961] | 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 ] |
[962] | Glen Mével, Jacques-Henri Jourdan, and François Pottier. Time credits and time receipts in Iris. In Luis Caires, editor, European Symposium on Programming (ESOP), volume 11423 of Lecture Notes in Computer Science, pages 1--27. Springer, April 2019. [ bib | .pdf ] |
[963] | Rasmus Ejlers Møgelberg and Sam Staton. Full abstraction in a metalanguage for state. In Workshop on Syntax and Semantics of Low Level Languages, July 2010. [ bib ] |
[964] | 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 ] |
[965] | 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 ] |
[966] | Gopalan Nadathur and Dale Miller. An overview of lambda-prolog. In Logic Programming, pages 810--827, August 1988. [ bib | http ] |
[967] | Gopalan Nadathur and Xiaochu Qi. Explicit substitutions in the reduction of lambda terms. In Principles and Practice of Declarative Programming (PPDP), pages 195--206, August 2003. [ bib | .ps ] |
[968] | Karl Naden, Robert Bocchino, Jonathan Aldrich, and Kevin Bierhoff. A type system for borrowing permissions. In Principles of Programming Languages (POPL), pages 557--570, January 2012. [ bib | .pdf ] |
[969] | Maurice Naftalin and Philip Wadler. Java generics and collections. O'Reilly, 2006. [ bib | http ] |
[970] | Hiroshi Nakano. A modality for recursion. In Logic in Computer Science (LICS), pages 255--266, June 2000. [ bib | .ps.gz ] |
[971] | Hiroshi Nakano. Fixed-point logic with the approximation modality and its Kripke completeness. In International Symposium on Theoretical Aspects of Computer Software (TACS), volume 2215 of Lecture Notes in Computer Science, pages 165--182. Springer, October 2001. [ bib | .pdf ] |
[972] | 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 ] |
[973] | Aleksandar Nanevski, Amal Ahmed, Greg Morrisett, and Lars Birkedal. Abstract predicates and mutable ADTs in Hoare type theory. In European Symposium on Programming (ESOP), volume 4421 of Lecture Notes in Computer Science, pages 189--204. Springer, March 2007. [ bib | .pdf ] |
[974] | Aleksandar Nanevski, Greg Morrisett, and Lars Birkedal. Polymorphism and separation in Hoare type theory. In International Conference on Functional Programming (ICFP), pages 62--73, September 2006. [ bib | .pdf ] |
[975] | Aleksandar Nanevski, Greg Morrisett, and Lars Birkedal. Hoare type theory, polymorphism and separation. Journal of Functional Programming, 18(5--6):865--911, 2008. [ bib | .pdf ] |
[976] | Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, and Lars Birkedal. Ynot: dependent types for imperative programs. In International Conference on Functional Programming (ICFP), pages 229--240, September 2008. [ bib | .pdf ] |
[977] | Aleksandar Nanevski, Viktor Vafeiadis, and Josh Berdine. Structuring the verification of heap-manipulating programs. In Principles of Programming Languages (POPL), pages 261--274, January 2010. [ bib | .pdf ] |
[978] | Wolfgang Naraschewski and Tobias Nipkow. Type inference verified: Algorithm W in Isabelle/HOL. Journal of Automated Reasoning, 23:299--318, 1999. [ bib | .ps.gz ] |
[979] | David A. Naumann. On assertion-based encapsulation for object invariants and simulations. Formal Aspects of Computing, 19(2):205--224, 2007. [ bib | .pdf ] |
[980] | Juan Antonio Navarro Pérez and Andrey Rybalchenko. Separation logic + superposition calculus = heap theorem prover. In Programming Language Design and Implementation (PLDI), pages 556--566, June 2011. [ bib | .pdf ] |
[981] | Pierre Neron, Andrew P. Tolmach, Eelco Visser, and Guido Wachsmuth. A theory of name resolution. In European Symposium on Programming (ESOP), volume 9032 of Lecture Notes in Computer Science, pages 205--231. Springer, April 2015. [ bib | .pdf ] |
[982] | René Neumann. A framework for verified depth-first algorithms. In ATx/WInG: Joint Proceedings of the Workshops on Automated Theory eXploration and on Invariant Generation, volume 17 of EPiC Series, pages 36--45. EasyChair, June 2012. [ bib | http ] |
[983] | Huu Hai Nguyen, Cristina David, Shengchao Qin, and Wei-Ngan Chin. Automated verification of shape and size properties via separation logic. In Verification, Model Checking and Abstract Interpretation (VMCAI), volume 4349 of Lecture Notes in Computer Science, pages 251--266. Springer, January 2007. [ bib | .pdf ] |
[984] | Jan Nicklisch and Simon Peyton Jones. An exploration of modular programs. In Functional Programming Workshop, July 1996. [ bib | .ps.gz ] |
[985] | Joachim Niehren, Martin Müller, and Andreas Podelski. Inclusion constraints over non-empty sets of trees. In Theory and Practice of Software Development (TAPSOFT), volume 1214 of Lecture Notes in Computer Science, pages 217--231. Springer, April 1997. [ bib | .ps ] |
[986] | Joachim Niehren and Tim Priesnitz. Non-structural subtype entailment in automata theory. In International Symposium on Theoretical Aspects of Computer Software (TACS). Springer, October 2001. [ bib | .ps.gz ] |
[987] | Joachim Niehren and Tim Priesnitz. Non-structural subtype entailment in automata theory. Information and Computation, 186(2):319--354, 2003. [ bib | .pdf ] |
[988] | Lasse R. Nielsen. A denotational investigation of defunctionalization. Technical Report RS-00-47, BRICS, December 2000. [ bib | http ] |
[989] | Flemming Nielson and Hanne Riis Nielson. Two-level semantics and code generation. Theoretical Computer Science, 56(1):59--133, January 1988. [ bib | http ] |
[990] | Flemming Nielson, Hanne Riis Nielson, and Helmut Seidl. A succinct solver for ALFP. Nordic Journal of Computing, 9(4):335--372, 2002. [ bib | .pdf ] |
[991] | Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T). Journal of the ACM, 53(6):937--977, 2006. [ bib | .pdf ] |
[992] | Tobias Nipkow. Amortized complexity verified. In Interactive Theorem Proving (ITP), volume 9236 of Lecture Notes in Computer Science, pages 310--324. Springer, August 2015. [ bib | .pdf ] |
[993] | Susumu Nishimura. Static typing for dynamic messages. In Principles of Programming Languages (POPL), pages 266--278, January 1998. [ bib | .ps.gz ] |
[994] | Gian Ntzik and Philippa Gardner. Reasoning about the POSIX file system: local update and global pathnames. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 201--220, October 2015. [ bib | .pdf ] |
[995] | Russell O'Connor. Assembly: Circular programming with recursive do. The Monad.Reader, 6, January 2007. [ bib | .pdf ] |
[996] | Martin Odersky. Observers for linear types. In European Symposium on Programming (ESOP), volume 582 of Lecture Notes in Computer Science, pages 390--407. Springer, 1992. [ bib | .ps.gz ] |
[997] | Martin Odersky. A functional theory of local names. In Principles of Programming Languages (POPL), pages 48--59, January 1994. [ bib | .ps.gz ] |
[998] | 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 ] |
[999] | Martin Odersky and Konstantin Läufer. Putting type annotations to work. In Principles of Programming Languages (POPL), pages 54--67, January 1996. [ bib | .ps.gz ] |
[1000] | Martin Odersky, Lex Spoon, and Bill Venners. Programming in Scala, third edition: A comprehensive step-by-step guide. Artima Incorporation, 2016. [ bib | http ] |
[1001] | Martin Odersky, Martin Sulzmann, and Martin Wehr. Type inference with constrained types. Theory and Practice of Object Systems, 5(1):35--55, 1999. [ bib | .pdf ] |
[1002] | Martin Odersky, Philip Wadler, and Martin Wehr. A second look at overloading. In Functional Programming Languages and Computer Architecture (FPCA), pages 135--146, June 1995. [ bib | .ps.gz ] |
[1003] | 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 ] |
[1004] | Martin Odersky and Matthias Zenger. Scalable component abstractions. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 41--57, October 2005. [ bib | .pdf ] |
[1005] | Martin Odersky, Matthias Zenger, and Christoph Zenger. Colored local type inference. In Principles of Programming Languages (POPL), pages 41--53, 2001. [ bib | .ps.gz ] |
[1006] | Peter O'Hearn. On bunched typing. Journal of Functional Programming, 13(4):747--796, 2003. [ bib | .pdf ] |
[1007] | Peter W. O'Hearn. Resources, concurrency and local reasoning. Theoretical Computer Science, 375(1--3):271--307, May 2007. [ bib | .pdf ] |
[1008] | Peter W. O'Hearn, John Power, Makoto Takeyama, and Robert D. Tennent. Syntactic control of interference revisited. Theoretical Computer Science, 228(1-2):211--252, 1999. [ bib | http ] |
[1009] | Peter W. O'Hearn and John C. Reynolds. From Algol to polymorphic linear lambda-calculus. Journal of the ACM, 47(1):167--223, 2000. [ bib | .ps ] |
[1010] | Peter W. O'Hearn, Hongseok Yang, and John C. Reynolds. Separation and information hiding. In Principles of Programming Languages (POPL), pages 268--280, January 2004. [ bib | .pdf ] |
[1011] | Peter W. O'Hearn, Hongseok Yang, and John C. Reynolds. Separation and information hiding. ACM Transactions on Programming Languages and Systems, 31(3), 2009. [ bib | .pdf ] |
[1012] | Atsushi Ohori. A polymorphic record calculus and its compilation. ACM Transactions on Programming Languages and Systems, 17(6):844--895, November 1995. [ bib | http ] |
[1013] | 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 ] |
[1014] | Chris Okasaki. Purely functional data structures. Technical Report CMU-CS-96-177, School of Computer Science, Carnegie Mellon University, September 1996. [ bib | .pdf ] |
[1015] | Chris Okasaki. The role of lazy evaluation in amortized data structures. In International Conference on Functional Programming (ICFP), pages 62--72, May 1996. [ bib | .ps ] |
[1016] | Chris Okasaki. Views for Standard ML. In ACM Workshop on ML, pages 14--23, September 1998. [ bib | .ps ] |
[1017] | Chris Okasaki. Purely functional data structures. Cambridge University Press, 1999. [ bib | http ] |
[1018] | Chris Okasaki and Andy Gill. Fast mergeable integer maps. In ACM Workshop on ML, pages 77--86, September 1998. [ bib | .ps ] |
[1019] | 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 ] |
[1020] | Oswaldo Olivo, Isil Dillig, and Calvin Lin. Static detection of asymptotic performance bugs in collection traversals. In Programming Language Design and Implementation (PLDI), pages 369--378, June 2015. [ bib | .pdf ] |
[1021] | Peter Ørbæk and Jens Palsberg. Trust in the λ-calculus. Journal of Functional Programming, 7(6):557--591, November 1997. [ bib | .pdf ] |
[1022] | Joseph O'Rourke. Computational geometry in C, second edition. Cambridge University Press, 1998. [ bib | .html ] |
[1023] | James William O'Toole, Jr. and David K. Gifford. Type reconstruction with first-class polymorphic values. In Programming Language Design and Implementation (PLDI), pages 207--217, 1989. [ bib | .ps ] |
[1024] | Scott Owens, John H. Reppy, and Aaron Turon. Regular-expression derivatives re-examined. Journal of Functional Programming, 19(2):173--190, 2009. [ bib | .pdf ] |
[1025] | David Pager. A practical general method for constructing LR(k) parsers. Acta Informatica, 7:249--268, 1977. [ bib | http ] |
[1026] | Robert Paige and Fritz Henglein. Mechanical translation of set theoretic problem specifications into efficient RAM code -- A case study. Journal of Symbolic Computation, 4(2):207--232, 1987. [ bib | http ] |
[1027] | Robert Paige and Robert E. Tarjan. Three partition refinement algorithms. SIAM Journal on Computing, 16(6):973--989, December 1987. [ bib | .pdf ] |
[1028] | Jens Palsberg. Efficient inference of object types. Information and Computation, 123(2):198--209, 1995. [ bib | .pdf ] |
[1029] | 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 ] |
[1030] | 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 ] |
[1031] | 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 ] |
[1032] | 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 ] |
[1033] | Jens Palsberg and Tian Zhao. Efficient and flexible matching of recursive types. Information and Computation, 171:364--387, 2001. [ bib | .pdf ] |
[1034] | Jens Palsberg and Tian Zhao. Efficient type inference for record concatenation and subtyping. In Logic in Computer Science (LICS), pages 125--136, July 2002. [ bib ] |
[1035] | Jens Palsberg and Tian Zhao. Type inference for record concatenation and subtyping. Information and Computation, 189:54--86, 2004. [ bib | .pdf ] |
[1036] | Matthew Parkinson and Gavin Bierman. Separation logic and abstraction. In Principles of Programming Languages (POPL), pages 247--258, January 2005. [ bib | http ] |
[1037] | Matthew Parkinson and Gavin Bierman. Separation logic, abstraction and inheritance. In Principles of Programming Languages (POPL), pages 75--86, January 2008. [ bib | http ] |
[1038] | David Lorge Parnas. Information distribution aspects of design methodology. In Information Processing 71, volume 1, pages 339--344, 1971. [ bib | .PDF ] |
[1039] | David Lorge Parnas. On the criteria to be used in decomposing systems into modules. Communications of the ACM, 15(12):1053--1058, 1972. [ bib | http ] |
[1040] | Terence Parr. The definitive ANTLR 4 reference, 2nd edition. Pragmatic Bookshelf, 2013. [ bib ] |
[1041] | Pašalić and Nathan Linger. Meta-programming with typed object-language representations. In Generative Programming and Component Engineering (GPCE), pages 136--167, October 2004. [ bib | .ps ] |
[1042] | 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 ] |
[1043] | Emir Pašalić, Walid Taha, and Tim Sheard. Tagless staged interpreters for typed languages. In International Conference on Functional Programming (ICFP), pages 218--229, October 2002. [ bib | .pdf ] |
[1044] | M. S. Paterson and M. N. Wegman. Linear unification. In Annual ACM Symposium on Theory of Computing, pages 181--186, 1976. [ bib ] |
[1045] | Md. Mostofa Ali Patwary, Jean Blair, and Fredrik Manne. Experiments on union-find algorithms for the disjoint-set data structure. In International Symposium on Experimental Algorithms (SEA), volume 6049 of Lecture Notes in Computer Science, pages 411--423. Springer, May 2010. [ bib | .pdf ] |
[1046] | Christine Paulin-Mohring. Extracting F_{ω}'s programs from proofs in the calculus of constructions. In Principles of Programming Languages (POPL), pages 89--104, January 1989. [ bib | http ] |
[1047] | Christine Paulin-Mohring. Inductive definitions in the system Coq: rules and properties. Research Report RR1992-49, ENS Lyon, 1992. [ bib | .ps.Z ] |
[1048] | Thomas J. Pennello. Very fast LR parsing. In Symposium on Compiler Construction, pages 145--151, 1986. [ bib | http ] |
[1049] | 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 ] |
[1050] | John Peterson and Mark P. Jones. Implementing type classes. In Programming Language Design and Implementation (PLDI), pages 227--236, June 1993. [ bib | .ps ] |
[1051] | Simon Peyton Jones. The implementation of functional programming languages. Prentice Hall, 1987. [ bib | http ] |
[1052] | Simon Peyton Jones, editor. Haskell 98 language and libraries: The revised report. Cambridge University Press, April 2003. [ bib | http ] |
[1053] | Simon Peyton Jones. Tackling the awkward squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell. Online lecture notes, January 2009. [ bib | .pdf ] |
[1054] | Simon Peyton Jones and Simon Marlow. Secrets of the Glasgow Haskell Compiler inliner. Journal of Functional Programming, 12(4&5):393--433, 2002. [ bib | .ps.gz ] |
[1055] | Simon Peyton Jones and Mark Shields. Lexically-scoped type variables. Manuscript, April 2004. [ bib | http ] |
[1056] | Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields. Practical type inference for arbitrary-rank types. Journal of Functional Programming, 17(1):1--82, 2007. [ bib | .pdf ] |
[1057] | Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. Simple unification-based type inference for GADTs. In International Conference on Functional Programming (ICFP), pages 50--61, September 2006. [ bib | .pdf ] |
[1058] | Simon Peyton Jones and Philip Wadler. Imperative functional programming. In Principles of Programming Languages (POPL), pages 71--84, January 1993. [ bib | .ps.gz ] |
[1059] | 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 ] |
[1060] | Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In Programming Language Design and Implementation (PLDI), pages 199--208, June 1988. [ bib | http ] |
[1061] | Frank Pfenning and Peter Lee. LEAP: A language with eval and polymorphism. In Theory and Practice of Software Development (TAPSOFT), volume 352 of Lecture Notes in Computer Science, pages 345--359. Springer, 1989. [ bib | http ] |
[1062] | Brigitte Pientka. Proof pearl: The power of higher-order encodings in the logical framework LF. In Theorem Proving in Higher Order Logics (TPHOLs), volume 4732 of Lecture Notes in Computer Science, pages 246--261. Springer, September 2007. [ bib | .pdf ] |
[1063] | Brigitte Pientka. A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In Principles of Programming Languages (POPL), pages 371--382, January 2008. [ bib | .pdf ] |
[1064] | Brigitte Pientka and Joshua Dunfield. Programming with proofs and explicit contexts. In Principles and Practice of Declarative Programming (PPDP), pages 163--173, July 2008. [ bib | .pdf ] |
[1065] | Benjamin Pierce and Davide Sangiorgi. Typing and subtyping for mobile processes. In Logic in Computer Science (LICS), pages 376--385, June 1993. [ bib | .ps ] |
[1066] | Benjamin C. Pierce. Bounded quantification is undecidable. Information and Computation, 112(1):131--165, July 1994. [ bib | .ps ] |
[1067] | Benjamin C. Pierce. Types and programming languages. MIT Press, 2002. [ bib | http ] |
[1068] | Benjamin C. Pierce. Types and programming languages. MIT Press, 2002. [ bib ] |
[1069] | 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 ] |
[1070] | 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 ] |
[1071] | 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 ] |
[1072] | Alexandre Pilkiewicz and François Pottier. The essence of monotonic state. In Types in Language Design and Implementation (TLDI), January 2011. [ bib | .pdf ] |
[1073] | Ruzica Piskac, Thomas Wies, and Damien Zufferey. Automating separation logic using SMT. In Computer Aided Verification (CAV), volume 8044 of Lecture Notes in Computer Science, pages 773--789. Springer, July 2013. [ bib | .pdf ] |
[1074] | Ruzica Piskac, Thomas Wies, and Damien Zufferey. Automating separation logic with trees and data. In Computer Aided Verification (CAV), volume 8559 of Lecture Notes in Computer Science, pages 711--728. Springer, July 2014. [ bib | .pdf ] |
[1075] | Andrew M. Pitts. Parametric polymorphism and operational equivalence. Mathematical Structures in Computer Science, 10:321--359, 2000. [ bib | .pdf ] |
[1076] | Andrew M. Pitts. Nominal logic, A first order theory of names and binding. Information and Computation, 186:165--193, 2003. [ bib | .pdf ] |
[1077] | Andrew M. Pitts. Alpha-structural recursion and induction. In Theorem Proving in Higher Order Logics (TPHOLs), Lecture Notes in Computer Science. Springer, August 2005. [ bib | .pdf ] |
[1078] | Andrew M. Pitts. Alpha-structural recursion and induction. Journal of the ACM, 53:459--506, 2006. [ bib | .pdf ] |
[1079] | Andrew M. Pitts. Nominal System T. In Principles of Programming Languages (POPL), pages 159--170, January 2010. [ bib | .pdf ] |
[1080] | Andrew M. Pitts and Murdoch J. Gabbay. A metalanguage for programming with bound names modulo renaming. In Mathematics of Program Construction (MPC), volume 1837 of Lecture Notes in Computer Science, pages 230--255. Springer, 2000. [ bib | .pdf ] |
[1081] | 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 ] |
[1082] | Gordon D. Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1(2):125--159, 1975. [ bib | .pdf ] |
[1083] | Gordon D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5(3):225--255, 1977. [ bib | .pdf ] |
[1084] | Nadia Polikarpova, Julian Tschannen, and Carlo A. Furia. A fully verified container library. In Formal Methods (FM), volume 9109 of Lecture Notes in Computer Science, pages 414--434. Springer, June 2015. [ bib | .pdf ] |
[1085] | Randy Pollack, Masahiko Sato, and Wilmer Ricciotti. A canonical locally named representation of binding. Journal of Automated Reasoning, 49(2):185--207, 2012. [ bib | .pdf ] |
[1086] | Satya Kiran Popuri. Understanding C parsers generated by GNU Bison, September 2006. [ bib | .html ] |
[1087] | Adam Poswolsky and Carsten Schürmann. Practical programming with higher-order encodings and dependent types. In European Symposium on Programming (ESOP), volume 4960 of Lecture Notes in Computer Science, pages 93--107. Springer, March 2008. [ bib | .pdf ] |
[1088] | Adam Poswolsky and Carsten Schürmann. System description: Delphin -- A functional programming language for deductive systems. Electronic Notes in Theoretical Computer Science, 228:113--120, 2009. [ bib | .pdf ] |
[1089] | Alex Potanin, Johan Östlund, Yoav Zibin, and Michael D. Ernst. Immutability. In Aliasing in Object-Oriented Programming. Types, Analysis and Verification, volume 7850 of Lecture Notes in Computer Science, pages 233--269. Springer, 2013. [ bib | .pdf ] |
[1090] | François Pottier. Implémentation d'un système de modules évolué en Caml-Light. Research Report 2449, INRIA, 1995. [ bib | .ps.gz ] |
[1091] | 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 ] |
[1092] | François Pottier. Simplifying subtyping constraints. In International Conference on Functional Programming (ICFP), pages 122--133, January 1996. [ bib | .ps.gz ] |
[1093] | François Pottier. A framework for type inference with subtyping. In International Conference on Functional Programming (ICFP), pages 228--238, September 1998. [ bib | .ps.gz ] |
[1094] | 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 ] |
[1095] | François Pottier. Type inference in the presence of subtyping: from theory to practice. Research Report 3483, INRIA, September 1998. [ bib | .pdf ] |
[1096] | 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, March 2000. [ bib | .ps.gz ] |
[1097] | François Pottier. A versatile constraint-based type inference system. Nordic Journal of Computing, 7(4):312--347, November 2000. [ bib | .ps.gz ] |
[1098] | François Pottier. Wallace: an efficient implementation of type inference with subtyping, February 2000. [ bib | http ] |
[1099] | François Pottier. A semi-syntactic soundness proof for HM(X). Research Report 4150, INRIA, March 2001. [ bib | .pdf ] |
[1100] | François Pottier. Simplifying subtyping constraints: a theory. Information and Computation, 170(2):153--183, November 2001. [ bib | .ps.gz ] |
[1101] | 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 ] |
[1102] | François Pottier. A constraint-based presentation and generalization of rows. In Logic in Computer Science (LICS), pages 331--340, June 2003. [ bib | .ps.gz ] |
[1103] | François Pottier. Cαml, June 2005. [ bib | http ] |
[1104] | 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 ] |
[1105] | François Pottier. Static name control for FreshML. In Logic in Computer Science (LICS), pages 356--365, July 2007. [ bib | .pdf ] |
[1106] | François Pottier. Hiding local state in direct style: a higher-order anti-frame rule. In Logic in Computer Science (LICS), pages 331--340, June 2008. [ bib | .pdf ] |
[1107] | François Pottier. Generalizing the higher-order frame and anti-frame rules. Unpublished, July 2009. [ bib | .pdf ] |
[1108] | François Pottier. Lazy least fixed points in ML. Unpublished, December 2009. [ bib | .pdf ] |
[1109] | François Pottier. Three comments on the anti-frame rule. Unpublished, July 2009. [ bib | .pdf ] |
[1110] | François Pottier. Syntactic soundness proof of a type-and-capability system with hidden state. Journal of Functional Programming, 23(1):38--144, January 2013. [ bib | .pdf ] |
[1111] | François Pottier. Depth-first search and strong connectivity in Coq. In Journées Françaises des Langages Applicatifs (JFLA), January 2015. [ bib | .pdf ] |
[1112] | François Pottier. Reachability and error diagnosis in LR(1) automata. In Journées Françaises des Langages Applicatifs (JFLA), January 2016. [ bib | .pdf ] |
[1113] | François Pottier. Reachability and error diagnosis in LR(1) parsers. In Compiler Construction (CC), pages 88--98, March 2016. [ bib | .pdf ] |
[1114] | François Pottier. AlphaLib. https://gitlab.inria.fr/fpottier/alphaLib, 2017. [ bib ] |
[1115] | François Pottier. The visitors package. https://gitlab.inria.fr/fpottier/visitors, April 2017. [ bib ] |
[1116] | François Pottier. Verifying a hash table and its iterators in higher-order separation logic. In Certified Programs and Proofs (CPP), pages 3--16, January 2017. [ bib | .pdf ] |
[1117] | François Pottier and Sylvain Conchon. Information flow inference for free. In International Conference on Functional Programming (ICFP), pages 46--57, September 2000. [ bib | .ps.gz ] |
[1118] | François Pottier and Nadji Gauthier. Polymorphic typed defunctionalization. In Principles of Programming Languages (POPL), pages 89--98, January 2004. [ bib | .pdf ] |
[1119] | François Pottier and Nadji Gauthier. Polymorphic typed defunctionalization and concretization. Higher-Order and Symbolic Computation, 19:125--162, March 2006. [ bib | .pdf ] |
[1120] | François Pottier and Jonathan Protzenko. Programming with permissions in Mezzo. In International Conference on Functional Programming (ICFP), pages 173--184, September 2013. [ bib | .pdf ] |
[1121] | François Pottier and Jonathan Protzenko. A few lessons from the Mezzo project. In Summit on Advances in Programming Languages (SNAPL), May 2015. [ bib | .pdf ] |
[1122] | François Pottier and Yann Régis-Gianas. The Menhir parser generator. http://gallium.inria.fr/~fpottier/menhir/. [ bib ] |
[1123] | François Pottier and Yann Régis-Gianas. Stratified type inference for generalized algebraic data types. In Principles of Programming Languages (POPL), pages 232--244, January 2006. [ bib | .pdf ] |
[1124] | François Pottier and Yann Régis-Gianas. Towards efficient, typed LR parsers. Electronic Notes in Theoretical Computer Science, 148(2):155--180, 2006. [ bib | .pdf ] |
[1125] | François Pottier and Didier Rémy. The essence of ML type inference. Draft of an extended version. Unpublished, September 2003. [ bib | .pdf ] |
[1126] | 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 | .pdf ] |
[1127] | François Pottier and Vincent Simonet. Information flow inference for ML. In Principles of Programming Languages (POPL), pages 319--330, January 2002. [ bib | .ps.gz ] |
[1128] | 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 ] |
[1129] | 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, April 2001. [ bib | .ps.gz ] |
[1130] | François Pottier, Christian Skalka, and Scott Smith. A systematic approach to static access control. ACM Transactions on Programming Languages and Systems, 27(2):344--382, 2005. [ bib | .ps.gz ] |
[1131] | 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 ] |
[1132] | Nicolas Pouillard. Nameless, painless. In International Conference on Functional Programming (ICFP), pages 320--332, September 2011. [ bib | .pdf ] |
[1133] | Nicolas Pouillard and François Pottier. A fresh look at programming with names and binders. In International Conference on Functional Programming (ICFP), pages 217--228, September 2010. [ bib | .pdf ] |
[1134] | Nicolas Pouillard and François Pottier. A unified treatment of syntax with binders. Journal of Functional Programming, 22(4--5):614--704, September 2012. [ bib | .pdf ] |
[1135] | Vaughan Pratt and Jerzy Tiuryn. Satisfiability of inequalities in a poset. Fundamenta Informaticæ, 28(1--2):165--182, 1996. [ bib | .ps.gz ] |
[1136] | Matija Pretnar. An introduction to algebraic effects and handlers. Electronic Notes in Theoretical Computer Science, 319:19--35, 2015. [ bib | .pdf ] |
[1137] | Jonathan Protzenko. Mezzo: a typed language for safe effectful concurrent programs. PhD thesis, Université Paris Diderot, September 2014. [ bib | http ] |
[1138] | William Pugh and Grant Weddell. Two-directional record layout for multiple inheritance. In Programming Language Design and Implementation (PLDI), pages 85--91, 1990. [ bib | http ] |
[1139] | Paul Purdom. The size of LALR(1) parsers. BIT Numerical Mathematics, 14(3):326--337, 1974. [ bib | http ] |
[1140] | Zhenyu Qian. Unification of higher-order patterns in linear time and space. Journal of Logic and Computation, 6(3):315--341, 1996. [ bib ] |
[1141] | Christophe Raffalli. Type checking in system F^{η}. Prépublication 98-05a, LAMA, Université de Savoie, 1998. [ bib | .ps ] |
[1142] | Christophe Raffalli. An optimized complete semi-algorithm for system F^{η}. Unpublished, 1999. [ bib | .ps ] |
[1143] | Viswanath Ramachandran and Pascal Van Hentenryck. Incremental algorithms for constraint solving and entailment over rational trees. In Foundations of Software Technology and Theoretical Computer Science (FSTTCS), pages 205--217, 1993. [ bib ] |
[1144] | G. Ramalingam, Alex Varshavsky, John Field, Deepak Goyal, and Shmuel Sagiv. Deriving specialized program analyses for certifying component-client conformance. In Programming Language Design and Implementation (PLDI), pages 83--94, June 2002. [ bib | .pdf ] |
[1145] | Eric Reed. Patina: A formalization of the Rust programming language. Technical Report UW-CSE-15-03-02, University of Washington, March 2015. [ bib | .pdf ] |
[1146] | Franz Regensburger. HOLCF: Higher order logic of computable functions. In Theorem Proving in Higher Order Logics (TPHOLs), volume 971 of Lecture Notes in Computer Science, pages 293--307. Springer, September 1995. [ bib | .pdf ] |
[1147] | Jakob Rehof. Minimal typings in atomic subtyping. Technical Report D-278, Department of Computer Science, University of Copenhagen, 1996. [ bib | .ps.gz ] |
[1148] | Jakob Rehof. Minimal typings in atomic subtyping. In Principles of Programming Languages (POPL), pages 278--291, January 1997. [ bib | .ps ] |
[1149] | Jakob Rehof and Manuel Fähndrich. Type-based flow analysis: From polymorphic subtyping to CFL-reachability. In Principles of Programming Languages (POPL), pages 54--66, January 2001. [ bib | .ps ] |
[1150] | Brian Reistad and David K. Gifford. Static dependent costs for estimating execution time. In ACM Symposium on Lisp and Functional Programming (LFP), pages 65--78, 1994. [ bib | .pdf ] |
[1151] | Didier Rémy. Extending ML type system with a sorted equational theory. Technical Report 1766, INRIA, 1992. [ bib | .pdf ] |
[1152] | Didier Rémy. Projective ML. In ACM Symposium on Lisp and Functional Programming (LFP), pages 66--75, 1992. [ bib | .pdf ] |
[1153] | Didier Rémy. Syntactic theories and the algebra of record terms. Research Report 1869, INRIA, 1993. [ bib | .pdf ] |
[1154] | 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, April 1994. [ bib | .pdf ] |
[1155] | 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 | .pdf ] |
[1156] | 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 | .pdf ] |
[1157] | 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 ] |
[1158] | 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, March 1998. [ bib | .pdf ] |
[1159] | Didier Rémy and Jérôme Vouillon. Objective ML: A simple object-oriented extension of ML. In Principles of Programming Languages (POPL), pages 40--53, January 1997. [ bib | .pdf ] |
[1160] | 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 | .pdf ] |
[1161] | Didier Rémy and Boris Yakobowski. A Church-style intermediate language for MLF. Theoretical Computer Science, 435(1):77--105, June 2012. [ bib | .pdf ] |
[1162] | Thomas Reps. Program analysis via graph reachability. Information and Software Technology, 40(11--12):701--726, 1998. [ bib | .pdf ] |
[1163] | William S. Retert. Implementing permission analysis. PhD thesis, University of Wisconsin-Milwaukee, May 2009. [ bib ] |
[1164] | 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, September 2006. [ bib | .pdf ] |
[1165] | Dominique Revuz. Minimization of acyclic deterministic automata in linear time. Theoretical Computer Science, 92(1):181--189, 1992. [ bib ] |
[1166] | John C. Reynolds. Automatic computation of data set definitions. In Information Processing 68, volume 1, pages 456--461. North Holland, 1969. [ bib ] |
[1167] | 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, April 1974. [ bib | http ] |
[1168] | John C. Reynolds. User-defined types and procedural data structures as complementary approaches to data abstraction. Technical Report 1278, Carnegie Mellon University, August 1975. [ bib | http ] |
[1169] | John C. Reynolds. Syntactic control of interference. In Principles of Programming Languages (POPL), pages 39--46, January 1978. [ bib | http ] |
[1170] | John C. Reynolds. Types, abstraction and parametric polymorphism. In Information Processing 83, pages 513--523. Elsevier Science, 1983. [ bib | .pdf ] |
[1171] | John C. Reynolds. Three approaches to type structure. In Theory and Practice of Software Development (TAPSOFT), volume 185 of Lecture Notes in Computer Science, pages 97--138. Springer, March 1985. [ bib | http ] |
[1172] | 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 | http ] |
[1173] | John C. Reynolds. The discoveries of continuations. Lisp and Symbolic Computation, 6(3--4):233--248, 1993. [ bib | .pdf ] |
[1174] | John C. Reynolds. User defined types and procedural data structures as complementary approaches to data abstraction. In Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects Of Object-Oriented Programming: Types, Semantics and Language Design, pages 13--23. MIT Press, 1994. [ bib ] |
[1175] | John C. Reynolds. Definitional interpreters for higher-order programming languages. Higher-Order and Symbolic Computation, 11(4):363--397, December 1998. [ bib | http ] |
[1176] | John C. Reynolds. Definitional interpreters revisited. Higher-Order and Symbolic Computation, 11(4):355--361, December 1998. [ bib | http ] |
[1177] | John C. Reynolds. Separation logic: A logic for shared mutable data structures. In Logic in Computer Science (LICS), pages 55--74, 2002. [ bib | .pdf ] |
[1178] | Morten Rhiger. A foundation for embedded languages. ACM Transactions on Programming Languages and Systems, 25(3):291--315, May 2003. [ bib | http ] |
[1179] | Colin Riba. On the values of reducibility candidates. In Typed Lambda Calculi and Applications (TLCA), volume 5608 of Lecture Notes in Computer Science, pages 264--278. Springer, July 2009. [ bib | .pdf ] |
[1180] | Michael F. Ringenburg and Dan Grossman. Types for describing coordinated data structures. In Types in Language Design and Implementation (TLDI), pages 25--36, January 2005. [ bib | .pdf ] |
[1181] | Mikael Rittri. Using types as search keys in function libraries. Journal of Functional Programming, 1(1):71--89, 1991. [ bib ] |
[1182] | Mikael Rittri. Retrieving library functions by unifying types modulo linear isomorphism. RAIRO Theoretical Informatics and Applications, 27(6):523--540, 1993. [ bib ] |
[1183] | Xavier Rival. Abstract domains for the static analysis of programs manipulating complex data structures. Habilitation à diriger des recherches, École Normale Supérieure, 2011. [ bib | .pdf ] |
[1184] | J. Alan Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23--41, 1965. [ bib | http ] |
[1185] | Tiark Rompf and Nada Amin. Type soundness for dependent object types (DOT). In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 624--641, November 2016. [ bib | .pdf ] |
[1186] | Mads Rosendahl. Automatic complexity analysis. In Functional Programming Languages and Computer Architecture (FPCA), pages 144--156, 1989. [ bib | http ] |
[1187] | 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 ] |
[1188] | Andreas Rossberg. 1ML -- core and modules united (F-ing first-class modules). In International Conference on Functional Programming (ICFP), pages 35--47, September 2015. [ bib | .pdf ] |
[1189] | Andreas Rossberg, Claudio V. Russo, and Derek Dreyer. F-ing modules. Journal of Functional Programming, 24(5):529--607, 2014. [ bib | .pdf ] |
[1190] | Andreas Rossberg, Peter J. Stuckey, Martin Sulzmann, and Jeremy Wazny. The Chameleon language. [ bib | http ] |
[1191] | Colin Runciman and Ian Toyn. Retrieving re-usable software components by polymorphic type. Journal of Functional Programming, 1(2):191--211, 1991. [ bib ] |
[1192] | Stuart Russell and Peter Norvig. Artificial intelligence: A modern approach. Prentice Hall, 2009. [ bib | http ] |
[1193] | Claudio V. Russo. Types for modules. PhD thesis, University of Edinburgh, 1998. [ bib | .html ] |
[1194] | Yann Régis-Gianas. Des types aux assertions logiques : preuve automatique ou assistée de propriétés sur les programmes fonctionnels. PhD thesis, Université Paris 7, November 2007. [ bib | .pdf ] |
[1195] | Yann Régis-Gianas. The Pangolin programming language, 2008. http://code.google.com/p/pangolin-programming-language/. [ bib | http ] |
[1196] | Yann Régis-Gianas and François Pottier. A Hoare logic for call-by-value functional programs. In Mathematics of Program Construction (MPC), volume 5133 of Lecture Notes in Computer Science, pages 305--335. Springer, July 2008. [ bib | .pdf ] |
[1197] | Didier Rémy. Type checking records and variants in a natural extension of ML. In Principles of Programming Languages (POPL), pages 77--88, 1989. [ bib | http ] |
[1198] | Didier Rémy. Efficient representation of extensible records. In ACM Workshop on ML and its Applications, June 1992. [ bib | .pdf ] |
[1199] | Didier Rémy. Simple, partial type inference for system F based on type containment. In International Conference on Functional Programming (ICFP), September 2005. [ bib | .pdf ] |
[1200] | Didier Rémy. Simple, partial type inference for system F based on type containment. In International Conference on Functional Programming (ICFP), September 2005. [ bib | .pdf ] |
[1201] | 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, 1999. [ bib | .ps ] |
[1202] | Daniel Sabin and Eugene C. Freuder. Contradicting conventional wisdom in constraint satisfaction. In International Workshop on Principles and Practice of Constraint Programming (PPCP), volume 874 of Lecture Notes in Computer Science, pages 10--20. Springer, May 1994. [ bib | .pdf ] |
[1203] | Amr Sabry. What is a purely functional language? Journal of Functional Programming, 8(1):1--22, January 1998. [ bib | http ] |
[1204] | Amr Sabry and Matthias Felleisen. Reasoning about programs in continuation-passing style. Lisp and Symbolic Computation, 6(3--4):289--360, 1993. [ bib | .ps.gz ] |
[1205] | Bratin Saha, Nevin Heintze, and Dino Oliva. Subtransitive CFA using types. Technical Report YALEU/DCS/TR-1166, Yale University, October 1998. [ bib | .ps.gz ] |
[1206] | Amr Hany Saleh, Georgios Karachalias, Matija Pretnar, and Tom Schrijvers. Explicit effect subtyping. In European Symposium on Programming (ESOP), volume 10801 of Lecture Notes in Computer Science, pages 327--354. Springer, April 2018. [ bib | .pdf ] |
[1207] | David Sands. Complexity analysis for a lazy higher-order language. In European Symposium on Programming (ESOP), volume 432 of Lecture Notes in Computer Science, pages 361--376. Springer, May 1990. [ bib | http ] |
[1208] | David Sands, Jörgen Gustavsson, and Andrew Moran. Lambda calculi and linear speedups. In The Essence of Computation, Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, volume 2566 of Lecture Notes in Computer Science, pages 60--84. Springer, 2002. [ bib | .pdf ] |
[1209] | Davide Sangiorgi. On the bisimulation proof method. Mathematical Structures in Computer Science, 8(5):447--479, 1998. [ bib | .ps.gz ] |
[1210] | Patrick M. Sansom. Time profiling a lazy functional compiler. In Functional Programming, Workshops in Computing. Springer, July 1993. [ bib | .ps.gz ] |
[1211] | Olivier Savary Belanger, Stefan Monnier, and Brigitte Pientka. Programming type-safe transformations using higher-order abstract syntax. In Certified Programs and Proofs (CPP), volume 8307 of Lecture Notes in Computer Science, pages 243--258. Springer, December 2013. [ bib | http ] |
[1212] | Olivier Savary Belanger, Stefan Monnier, and Brigitte Pientka. Programming type-safe transformations using higher-order abstract syntax. Journal of Formalized Reasoning, 8(1), December 2015. [ bib | http ] |
[1213] | Steven Schäfer, Gert Smolka, and Tobias Tebbi. Completeness and decidability of de Bruijn substitution algebra in Coq. In Certified Programs and Proofs (CPP), pages 67--73, January 2015. [ bib | http ] |
[1214] | Steven Schäfer, Tobias Tebbi, and Gert Smolka. Autosubst: Reasoning with de Bruijn terms and parallel substitutions. In Interactive Theorem Proving (ITP), volume 9236 of Lecture Notes in Computer Science, pages 359--374. Springer, August 2015. [ bib | .pdf ] |
[1215] | Karl Max Schimpf. Construction methods of LR parsers. PhD thesis, University of Pennsylvania, May 1981. [ bib | http ] |
[1216] | Fred B. Schneider. On concurrent programming. Springer, 1997. [ bib ] |
[1217] | Fred B. Schneider. Enforceable security policies. ACM Transactions on Information and System Security, 3(1):1--50, February 2000. [ bib | .pdf ] |
[1218] | 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, September 2002. [ bib | .ps ] |
[1219] | Lenhart K. Schubert, Mary Angela Papalaskaris, and Jay Taugher. Determining type, part, color, and time relationships. Computer, 16(10):53--60, October 1983. [ bib ] |
[1220] | Michael I. Schwartzbach. Polymorphic type inference. Technical Report BRICS-LS-95-3, BRICS, June 1995. [ bib | .ps.gz ] |
[1221] | Jan Schwinghammer, Lars Birkedal, François Pottier, Bernhard Reus, Kristian Støvring, and Hongseok Yang. A step-indexed Kripke model of hidden state. Mathematical Structures in Computer Science, January 2012. To appear. [ bib | .pdf ] |
[1222] | Jan Schwinghammer, Lars Birkedal, Bernhard Reus, and Hongseok Yang. Nested Hoare triples and frame rules for higher-order store. In Computer Science Logic, volume 5771 of Lecture Notes in Computer Science, pages 440--454. Springer, September 2009. [ bib | .pdf ] |
[1223] | Jan Schwinghammer, Lars Birkedal, and Kristian Støvring. A step-indexed Kripke model of hidden state via recursive properties on recursively defined metric spaces. In Foundations of Software Science and Computation Structures (FOSSACS), number 6604 in Lecture Notes in Computer Science, pages 305--319. Springer, March 2011. [ bib | .pdf ] |
[1224] | Jan Schwinghammer, Hongseok Yang, Lars Birkedal, François Pottier, and Bernhard Reus. A semantic foundation for hidden state. In Foundations of Software Science and Computation Structures (FOSSACS), volume 6014 of Lecture Notes in Computer Science, pages 2--17. Springer, March 2010. [ bib | .pdf ] |
[1225] | Stefan Schwoon. Model-checking pushdown systems. PhD thesis, Technische Universität München, 2002. [ bib | .pdf ] |
[1226] | 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 ] |
[1227] | Carsten Schürmann, Adam Poswolsky, and Jeffrey Sarnat. The -calculus: Functional programming with higher-order encodings. In Typed Lambda Calculi and Applications (TLCA), volume 3461 of Lecture Notes in Computer Science, pages 339--353. Springer, April 2005. [ bib | .pdf ] |
[1228] | Dana S. Scott. A type-theoretical alternative to ISWIM, CUCH, OWHY. Theoretical Computer Science, 121(1--2):411--440, 1993. [ bib | http ] |
[1229] | Robert Sedgewick and Michael Schidlowsky. Algorithms in Java: Graph algorithms. Addison-Wesley, 2003. [ bib ] |
[1230] | Raimund Seidel and Micha Sharir. Top-down analysis of path compression. SIAM Journal on Computing, 34(3):515--525, 2005. [ bib | http ] |
[1231] | R. C. Sekar, R. Ramesh, and I. V. Ramakrishnan. Adaptive pattern matching. SIAM Journal on Computing, 24(6):1207--1234, December 1995. [ bib | .ps ] |
[1232] | Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. Mechanized verification of fine-grained concurrent programs. In Programming Language Design and Implementation (PLDI), pages 77--87, June 2015. [ bib | .pdf ] |
[1233] | 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 ] |
[1234] | 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 ] |
[1235] | Peter Sewell and Jan Vitek. Secure composition of untrusted code: Wrappers and causality types. In IEEE Computer Security Foundations Workshop, July 2000. [ bib | .ps ] |
[1236] | Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and Rok Strnisa. Ott: Effective tool support for the working semanticist. Journal of Functional Programming, 20(1):71--122, 2010. [ bib | .pdf ] |
[1237] | Edwin Hsing-Mean Sha and Kenneth Steiglitz. Maintaining bipartite matchings in the presence of failures. Networks, 23(5):459--471, August 1993. [ bib | .ps ] |
[1238] | 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 ] |
[1239] | Tim Sheard. Using MetaML: A staged programming language. In Advanced Functional Programming, volume 1608 of Lecture Notes in Computer Science, pages 207--239. Springer, September 1998. [ bib | .ps ] |
[1240] | 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, 2001. [ bib | .pdf ] |
[1241] | Tim Sheard. Languages of the future. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 116--119, October 2004. [ bib | http ] |
[1242] | Tim Sheard. Ωmega, November 2005. [ bib | http ] |
[1243] | Tim Sheard. Putting Curry-Howard to work. In Haskell workshop, pages 74--85, September 2005. [ bib | .ps ] |
[1244] | 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 ] |
[1245] | Tim Sheard and Simon Peyton Jones. Template metaprogramming for Haskell. In Haskell workshop, pages 1--16, October 2002. [ bib | .pdf ] |
[1246] | Mark B. Shields and Simon Peyton Jones. First class modules for Haskell. In Foundations of Object-Oriented Languages (FOOL), pages 28--40, January 2002. [ bib | .pdf ] |
[1247] | Mark R. Shinwell. The fresh approach: functional programming with names and binders. PhD thesis, University of Cambridge, February 2005. [ bib | .pdf ] |
[1248] | Mark R. Shinwell. Fresh O'Caml: nominal abstract syntax for the masses. Electronic Notes in Theoretical Computer Science, 148(2):53--77, 2006. [ bib | http ] |
[1249] | Mark R. Shinwell and Andrew M. Pitts. Fresh Objective Caml user manual. Technical Report 621, University of Cambridge, February 2005. [ bib | .pdf ] |
[1250] | Mark R. Shinwell and Andrew M. Pitts. On a monadic semantics for freshness. Theoretical Computer Science, 342:28--55, 2005. [ bib | .pdf ] |
[1251] | Mark R. Shinwell, Andrew M. Pitts, and Murdoch J. Gabbay. FreshML: Programming with binders made simple. In International Conference on Functional Programming (ICFP), pages 263--274, August 2003. [ bib | .pdf ] |
[1252] | 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, 1996. [ bib | .ps ] |
[1253] | 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 ] |
[1254] | Vincent Simonet. An extension of HM(X) with bounded existential and universal data-types. In International Conference on Functional Programming (ICFP), June 2003. [ bib | .ps.gz ] |
[1255] | Vincent Simonet. The Flow Caml system: documentation and user's manual. Technical Report 0282, INRIA, July 2003. [ bib | http ] |
[1256] | 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, November 2003. [ bib | .pdf ] |
[1257] | Vincent Simonet. Inférence de flots d'information pour ML: formalisation et implantation. PhD thesis, Université Paris 7, March 2004. [ bib | .pdf ] |
[1258] | Vincent Simonet and François Pottier. Constraint-based type inference for guarded algebraic data types. Research Report 5462, INRIA, January 2005. [ bib | .html ] |
[1259] | Christian Skalka. Types for programming language-based security. PhD thesis, The Johns Hopkins University, August 2002. [ bib | .ps ] |
[1260] | 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 ] |
[1261] | Christian Skalka and Scott Smith. Static enforcement of security with types. In International Conference on Functional Programming (ICFP), pages 34--45, September 2000. [ bib | .ps ] |
[1262] | Jan Smans, Bart Jacobs, and Frank Piessens. Implicit dynamic frames: Combining dynamic frames and separation logic. In European Conference on Object-Oriented Programming (ECOOP), volume 5653 of Lecture Notes in Computer Science, pages 148--172. Springer, July 2009. [ bib | .pdf ] |
[1263] | Sjaak Smetsers, Erik Barendsen, Marko C. J. D. van Eekelen, and Marinus J. Plasmeijer. Guaranteeing safe destructive updates through a type system with uniqueness information for graphs. In Dagstuhl Seminar on Graph Transformations in Computer Science, volume 776 of Lecture Notes in Computer Science, pages 358--379. Springer, 1994. [ bib | .pdf ] |
[1264] | 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, March 2000. [ bib | .pdf ] |
[1265] | Geoffrey Smith and Dennis Volpano. Secure information flow in a multi-threaded imperative language. In Principles of Programming Languages (POPL), pages 355--364, January 1998. [ bib | .ps.Z ] |
[1266] | Geoffrey S. Smith. Polymorphic type inference with overloading and subtyping. In Theory and Practice of Software Development (TAPSOFT), volume 668 of Lecture Notes in Computer Science, pages 671--685. Springer, April 1993. [ bib | http ] |
[1267] | 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 ] |
[1268] | Geoffrey S. Smith. A new type system for secure information flow. In IEEE Computer Security Foundations Workshop, pages 115--125, June 2001. [ bib | .pdf ] |
[1269] | 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, March 2000. [ bib | .pdf ] |
[1270] | Scott Fraser Smith. Partial objects in type theory. PhD thesis, Cornell University, January 1989. [ bib | .pdf ] |
[1271] | Gert Smolka and Ralf Treinen. Records for logic programming. Journal of Logic Programming, 18(3):229--258, April 1994. [ bib | .ps ] |
[1272] | Michael B. Smyth and Gordon D. Plotkin. The category-theoretic solution of recursive domain equations. SIAM Journal on Computing, 11(4):761--783, 1982. [ bib | .pdf ] |
[1273] | Alan Snyder. Encapsulation and inheritance in object-oriented programming languages. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 38--45, 1986. [ bib | http ] |
[1274] | Jonathan Sobel and Daniel P. Friedman. Recycling continuations. In International Conference on Functional Programming (ICFP), pages 251--260, September 1998. [ bib | .ps ] |
[1275] | Eljas Soisalon-Soininen. Inessential error entries and their use in LR parser optimization. ACM Transactions on Programming Languages and Systems, 4(2):179--195, April 1982. [ bib | http ] |
[1276] | Marvin H. Solomon. Type definitions with parameters. In Principles of Programming Languages (POPL), pages 31--38, January 1978. [ bib | http ] |
[1277] | Sergei V. Soloviev. The category of finite sets and cartesian closed categories. Journal of Soviet Mathematics, 22(3):1387--1400, 1983. [ bib ] |
[1278] | Matthieu Sozeau. Subset coercions in Coq. In Types for Proofs and Programs, volume 4502, pages 237--252, 2006. [ bib | .pdf ] |
[1279] | Matthieu Sozeau. Program-ing finger trees in Coq. In International Conference on Functional Programming (ICFP), pages 13--24, September 2007. [ bib | .pdf ] |
[1280] | Matthieu Sozeau and Nicolas Tabareau. Universe polymorphism in Coq. In Interactive Theorem Proving (ITP), volume 8558 of Lecture Notes in Computer Science, pages 499--514. Springer, July 2014. [ bib | .pdf ] |
[1281] | Mike Spivey. A functional theory of exceptions. Science of Computer Programming, 14:25--42, 1990. [ bib ] |
[1282] | Akhilesh Srikanth, Burak Sahin, and William R. Harris. Complexity verification using guided theorem enumeration. In Principles of Programming Languages (POPL), pages 639--652, January 2017. [ bib | .pdf ] |
[1283] | R. Stata and M. Abadi. A type system for Java bytecode subroutines. In Principles of Programming Languages (POPL), pages 149--160, January 1998. [ bib | .html ] |
[1284] | Paul A. Steckler and Mitchell Wand. Lightweight closure conversion. ACM Transactions on Programming Languages and Systems, 19(1):48--86, 1997. [ bib | .ps ] |
[1285] | Bjarne Steensgaard. Points-to analysis in almost linear time. In Principles of Programming Languages (POPL), pages 32--41, January 1996. [ bib | .ps ] |
[1286] | 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, August 1995. [ bib | http ] |
[1287] | 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 ] |
[1288] | Gordon Stewart, Lennart Beringer, and Andrew W. Appel. Verified heap theorem prover by paramodulation. In International Conference on Functional Programming (ICFP), pages 3--14, September 2012. [ bib | .pdf ] |
[1289] | 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 ] |
[1290] | Christopher Strachey. Fundamental concepts in programming languages. Higher-Order and Symbolic Computation, 13(1--2):11--49, April 2000. [ bib | http ] |
[1291] | Robert E. Strom and Shaula Yemini. Typestate: A programming language concept for enhancing software reliability. IEEE Transactions on Software Engineering, 12(1):157--171, 1986. [ bib | .pdf ] |
[1292] | Peter J. Stuckey and Martin Sulzmann. A theory of overloading. In International Conference on Functional Programming (ICFP), pages 167--178, 2002. [ bib | http ] |
[1293] | Peter J. Stuckey, Martin Sulzmann, and Jeremy Wazny. Interactive type debugging in Haskell. In Haskell workshop, pages 72--83, 2003. [ bib | .pdf ] |
[1294] | 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 ] |
[1295] | Zhendong Su, Alexander Aiken, Joachim Niehren, Tim Priesnitz, and Ralf Treinen. The first-order theory of subtyping constraints. In Principles of Programming Languages (POPL), pages 203--216, January 2002. [ bib | .pdf ] |
[1296] | Martin Sulzmann. Designing record systems. Research Report YALEU/DCS/RR-1128, Yale University, April 1997. [ bib | .ps.gz ] |
[1297] | Martin Sulzmann. A general framework for Hindley/Milner type systems with constraints. PhD thesis, Yale University, Department of Computer Science, May 2000. [ bib | http ] |
[1298] | 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, March 2001. [ bib | .pdf ] |
[1299] | 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 ] |
[1300] | Martin Sulzmann, Martin Odersky, and Martin Wehr. Type inference with constrained types. In Foundations of Object-Oriented Languages (FOOL), January 1997. [ bib | .ps.gz ] |
[1301] | 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 ] |
[1302] | Eijiro Sumii. A complete characterization of observational equivalence in polymorphic lambda-calculus with general references. In Computer Science Logic, volume 5771 of Lecture Notes in Computer Science, pages 455--469. Springer, September 2009. [ bib | .pdf ] |
[1303] | Eijiro Sumii and Naoki Kobayashi. A generalized deadlock-free process calculus. In High-Level Concurrent Languages (HLCL), volume 16 of Electronic Notes in Theoretical Computer Science, pages 55--77. Elsevier Science, September 1998. [ bib | .ps ] |
[1304] | Kasper Svendsen and Lars Birkedal. Impredicative concurrent abstract predicates. In European Symposium on Programming (ESOP), volume 8410 of Lecture Notes in Computer Science, pages 149--168. Springer, April 2014. [ bib | .pdf ] |
[1305] | Kasper Svendsen, Lars Birkedal, and Matthew J. Parkinson. Joins: A case study in modular specification of a concurrent reentrant higher-order library. In European Conference on Object-Oriented Programming (ECOOP), volume 7920 of Lecture Notes in Computer Science, pages 327--351. Springer, July 2013. [ bib | .pdf ] |
[1306] | Kasper Svendsen, Lars Birkedal, and Matthew J. Parkinson. Modular reasoning about separation of concurrent data structures. In European Symposium on Programming (ESOP), volume 7792 of Lecture Notes in Computer Science, pages 169--188. Springer, March 2013. [ bib | .pdf ] |
[1307] | Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthik Bhargavan, and Jean Yang. Secure distributed programming with value-dependent types. In International Conference on Functional Programming (ICFP), pages 266--278, September 2011. [ bib | .pdf ] |
[1308] | 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 ] |
[1309] | S. Doaitse Swierstra and Luc Duponcheel. Deterministic, error-correcting combinator parsers. In Advanced Functional Programming, volume 1129 of Lecture Notes in Computer Science, pages 184--207. Springer, August 1996. [ bib | .pdf ] |
[1310] | Walid Taha. Multi-stage programming: Its theory and applications. PhD thesis, Oregon Graduate Institute, November 1999. [ bib | .pdf ] |
[1311] | Walid Taha. A gentle introduction to multi-stage programming. In Domain-Specific Program Generation (DSPG), volume 3016 of Lecture Notes in Computer Science, pages 30--50. Springer, November 2004. [ bib | .pdf ] |
[1312] | Walid Taha and Michael Florentin Nielsen. Environment classifiers. In Principles of Programming Languages (POPL), pages 26--37, January 2003. [ bib | .pdf ] |
[1313] | Masako Takahashi. Parallel reductions in λ-calculus. Information and Computation, 118(1):120--127, 1995. [ bib | http ] |
[1314] | Carolyn Talcott. A theory of binding structures and applications to rewriting. Theoretical Computer Science, 112(1):99--143, 1993. [ bib | http ] |
[1315] | Jean-Pierre Talpin and Pierre Jouvelot. The type and effect discipline. Information and Computation, 11(2):245--296, 1994. [ bib | .pdf ] |
[1316] | Gang Tan, Zhong Shao, Xinyu Feng, and Hongxu Cai. Weak updates and separation logic. In Asian Symposium on Programming Languages and Systems (APLAS), volume 5904 of Lecture Notes in Computer Science, pages 178--193. Springer, December 2009. [ bib | .pdf ] |
[1317] | Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, and Michael Norrish. A new verified compiler backend for CakeML. In International Conference on Functional Programming (ICFP), pages 60--73, September 2016. [ bib | .pdf ] |
[1318] | David R. Tarditi and Andrew W. Appel. ML-Yacc user's manual, April 2000. [ bib | http ] |
[1319] | Robert Tarjan. Depth-first search and linear graph algorithms. SIAM Journal on Computing, 1(2):146--160, June 1972. [ bib | http ] |
[1320] | Robert E. Tarjan. Class notes: Disjoint set union. 1999. [ bib | .pdf ] |
[1321] | Robert E. Tarjan and Jan van Leeuwen. Worst-case analysis of set union algorithms. Journal of the ACM, 31(2):245--281, April 1984. [ bib | http ] |
[1322] | Robert E. Tarjan and Mihalis Yannakakis. Simple linear-time algorithms to test chordality of graphs, test acyclicity of hypergraphs, and selectively reduce acyclic hypergraphs. SIAM Journal on Computing, 13(3):566--579, August 1984. [ bib | http ] |
[1323] | Robert Endre Tarjan. Efficiency of a good but not linear set union algorithm. Journal of the ACM, 22(2):215--225, April 1975. [ bib | .pdf ] |
[1324] | Robert Endre Tarjan. Applications of path compression on balanced trees. Journal of the ACM, 26(4):690--715, October 1979. [ bib | http ] |
[1325] | Robert Endre Tarjan. Amortized computational complexity. SIAM Journal on Algebraic and Discrete Methods, 6(2):306--318, 1985. [ bib | http ] |
[1326] | Robert Endre Tarjan. Algorithmic design. Communications of the ACM, 30(3):204--212, 1987. [ bib | http ] |
[1327] | Robert Endre Tarjan and Andrew Chi-Chih Yao. Storing a sparse table. Communications of the ACM, 22(11):606--611, 1979. [ bib | http ] |
[1328] | The GHC team. The Glasgow Haskell compiler, March 2005. [ bib | http ] |
[1329] | Robert D. Tennent and Dan Ghica. Abstract models of storage. Higher-Order and Symbolic Computation, 13:119--129, 2000. [ bib | http ] |
[1330] | Satish R. Thatté. Automated synthesis of interface adapters for reusable classes. In Principles of Programming Languages (POPL), pages 174--187, January 1994. [ bib | http ] |
[1331] | The Coq development team. The Coq proof assistant, 2019. [ bib | http ] |
[1332] | The Mozilla foundation. The Rust programming language, 2014. [ bib | http ] |
[1333] | Hayo Thielecke. Comparing control constructs by double-barrelled CPS. Higher-Order and Symbolic Computation, 15(2--3):141--160, 2002. [ bib | .pdf ] |
[1334] | Hayo Thielecke. From control effects to typed continuation passing. In Principles of Programming Languages (POPL), pages 139--149, January 2003. [ bib | .pdf ] |
[1335] | Hayo Thielecke. Frame rules from answer types for code pointers. In Principles of Programming Languages (POPL), pages 309--319, January 2006. [ bib | .pdf ] |
[1336] | Peter Thiemann. ML-style typing, lambda lifting, and partial evaluation. In Latin American Conference on Functional Programming, March 1999. [ bib | .ps.gz ] |
[1337] | Peter Thiemann. Enforcing security properties using type specialization. In European Symposium on Programming (ESOP), Lecture Notes in Computer Science. Springer, April 2001. [ bib | .ps.gz ] |
[1338] | Simon J. Thompson and Huiqing Li. Refactoring tools for functional languages. Journal of Functional Programming, 23(3):293--350, 2013. [ bib | http ] |
[1339] | Ye Henry Tian. Mechanically verifying correctness of CPS compilation. In Computing: The Australasian Theory Symposium (CATS), volume 51 of CRPIT, pages 41--51. Australian Computer Society, January 2006. [ bib | .pdf ] |
[1340] | Jerzy Tiuryn. Subtype inequalities. In Logic in Computer Science (LICS), pages 308--317, June 1992. [ bib ] |
[1341] | Jerzy Tiuryn and Pawel Urzyczyn. The subtyping problem for second-order types is undecidable. Information and Computation, 179(1):1--18, 2002. [ bib | http ] |
[1342] | Jerzy Tiuryn and Mitchell Wand. Type reconstruction with recursive types and atomic subtyping. In Theory and Practice of Software Development (TAPSOFT), volume 668 of Lecture Notes in Computer Science, pages 686--701. Springer, April 1993. [ bib | .dvi ] |
[1343] | Luca Della Toffola, Michael Pradel, and Thomas R. Gross. Synthesizing programs that expose performance bottlenecks. In Code Generation and Optimization (CGO), pages 314--326, February 2018. [ bib | .pdf ] |
[1344] | Mads Tofte. Operational semantics and polymorphic type inference. PhD thesis, University of Edinburgh, 1988. [ bib | .ps ] |
[1345] | 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 ] |
[1346] | Mads Tofte and Jean-Pierre Talpin. Implementation of the typed call-by-value λ-calculus using a stack of regions. In Principles of Programming Languages (POPL), pages 188--201, January 1994. [ bib | .pdf ] |
[1347] | Mads Tofte and Jean-Pierre Talpin. Region-based memory management. Information and Computation, 132(2):109--176, 1997. [ bib | .pdf ] |
[1348] | Andrew Tolmach. Combining closure conversion with closure analysis using algebraic types. In Types in Compilation (TIC), June 1997. [ bib | .ps ] |
[1349] | 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 ] |
[1350] | Rodney W. Topor. A note on error recovery in recursive descent parsers. ACM SIGPLAN Notices, 17(2):37--40, February 1982. [ bib | http ] |
[1351] | Jesse A. Tov and Riccardo Pucella. Stateful contracts for affine types. In European Symposium on Programming (ESOP), volume 6012 of Lecture Notes in Computer Science, pages 550--569. Springer, March 2010. [ bib | .pdf ] |
[1352] | Jesse A. Tov and Riccardo Pucella. Practical affine types. In Principles of Programming Languages (POPL), pages 447--458, January 2011. [ bib | http ] |
[1353] | 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, September 1996. [ bib | .pdf ] |
[1354] | Matthew S. Tschantz and Michael D. Ernst. Javari: adding reference immutability to Java. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 211--230, October 2005. [ bib | .pdf ] |
[1355] | 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 ] |
[1356] | Hideki Tsuiki. On typed calculi with a merge operator. In Foundations of Software Technology and Theoretical Computer Science (FSTTCS), volume 880 of Lecture Notes in Computer Science, pages 101--112. Springer, 1994. [ bib | .ps.gz ] |
[1357] | Thomas Tuerk. Local reasoning about while-loops. Unpublished, August 2010. [ bib | .pdf ] |
[1358] | David N. Turner. The polymorphic pi-calculus: Theory and implementation. PhD thesis, University of Edinburgh, 1995. [ bib | http ] |
[1359] | David N. Turner, Philip Wadler, and Christian Mossin. Once upon a type. In Functional Programming Languages and Computer Architecture (FPCA), pages 1--11. ACM Press, June 1995. [ bib | .dvi ] |
[1360] | Aaron Turon, Derek Dreyer, and Lars Birkedal. Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency. In International Conference on Functional Programming (ICFP), pages 377--390, September 2013. [ bib | .pdf ] |
[1361] | Christian Urban. Nominal techniques in Isabelle/HOL. Journal of Automated Reasoning, 40(4):327--356, 2008. [ bib | .pdf ] |
[1362] | Christian Urban and Tobias Nipkow. Nominal verification of algorithm W. Unpublished, March 2008. [ bib | .pdf ] |
[1363] | Christian Urban, Andrew Pitts, and Murdoch Gabbay. Nominal unification. Theoretical Computer Science, 323:473--497, 2004. [ bib | .pdf ] |
[1364] | Christian Urban and Christine Tasson. Nominal techniques in Isabelle/HOL. In International Conference on Automated Deduction (CADE), volume 3632 of Lecture Notes in Computer Science, pages 38--53. Springer, July 2005. [ bib | .ps ] |
[1365] | Viktor Vafeiadis. Concurrent separation logic and operational semantics. Electronic Notes in Theoretical Computer Science, 276:335--351, 2011. [ bib | .pdf ] |
[1366] | Eelis van der Weegen and James McKinna. A machine-checked proof of the average-case complexity of Quicksort in Coq. In Types for Proofs and Programs, volume 5497 of Lecture Notes in Computer Science, pages 256--271. Springer, March 2008. [ bib | .pdf ] |
[1367] | Vincent van Oostrom. Confluence by decreasing diagrams. Theoretical Computer Science, 126(2):259--280, April 1994. [ bib | .ps.Z ] |
[1368] | 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, September 1999. [ bib | .pdf ] |
[1369] | Mandana Vaziri and Daniel Jackson. Checking heap-manipulating procedures with a constraint solver. In Tools and Algorithms for Construction and Analysis of Systems (TACAS), volume 2619 of Lecture Notes in Computer Science. Springer, April 2003. [ bib | .pdf ] |
[1370] | Bart Vergauwen and Johan Lewi. Efficient local correctness checking for single and alternating Boolean equation systems. In International Colloquium on Automata, Languages and Programming, volume 820 of Lecture Notes in Computer Science, pages 304--315. Springer, 1994. [ bib | http ] |
[1371] | Bart Vergauwen, Johan Lewi, I. Avau, and A. Poté. Efficient computation of nested fix-points, with applications to model checking. In International Conference on Temporal Logic (ICTL), volume 827 of Lecture Notes in Computer Science, pages 165--179. Springer, July 1994. [ bib | http ] |
[1372] | Bart Vergauwen, J. Wauman, and Johan Lewi. Efficient fixpoint computation. In Static Analysis Symposium (SAS), volume 864 of Lecture Notes in Computer Science, pages 314--328. Springer, 1994. [ bib | http ] |
[1373] | Jules Villard, Étienne Lozes, and Cristiano Calcagno. Proving copyless message passing. In Asian Symposium on Programming Languages and Systems (APLAS), volume 5904 of Lecture Notes in Computer Science, pages 194--209. Springer, December 2009. [ bib | .pdf ] |
[1374] | Jules Villard, Étienne Lozes, and Cristiano Calcagno. Tracking heaps that hop with Heap-Hop. In Tools and Algorithms for Construction and Analysis of Systems (TACAS), volume 6015 of Lecture Notes in Computer Science, pages 275--279. Springer, March 2010. [ bib | .pdf ] |
[1375] | Jan Vitek and Boris Bokowski. Confined types in Java. Software: Practice and Experience, 31(6):507--532, 2001. [ bib | .pdf ] |
[1376] | Dennis Volpano. Provably-secure programming languages for remote evaluation. ACM SIGPLAN Notices, 32(1):117--119, January 1997. [ bib ] |
[1377] | 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 ] |
[1378] | 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 ] |
[1379] | 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 ] |
[1380] | 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, 1996. [ bib | .ps.Z ] |
[1381] | Jérôme Vouillon and Paul-André Melliès. Semantic types: a fresh look at the ideal model for types. In Principles of Programming Languages (POPL), pages 52--63, January 2004. [ bib | .ps.gz ] |
[1382] | Dimitrios Vytiniotis, Simon Peyton Jones, Tom Schrijvers, and Martin Sulzmann. OutsideIn(X): Modular type inference with local assumptions. Journal of Functional Programming, 21(4--5):333--412, 2011. [ bib | .pdf ] |
[1383] | Dimitrios Vytiniotis and Stephanie Weirich. Dependent types: Easy as PIE. In Trends in Functional Programming (TFP), April 2007. [ bib | .pdf ] |
[1384] | Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones. Boxy types: type inference for higher-rank types and impredicativity. Manuscript, April 2005. [ bib | http ] |
[1385] | Philip Wadler. Theorems for free! In Functional Programming Languages and Computer Architecture (FPCA), pages 347--359, September 1989. [ bib | .ps.gz ] |
[1386] | 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 ] |
[1387] | Philip Wadler. Comprehending monads. Mathematical Structures in Computer Science, 2:461--493, 1992. [ bib | .ps.gz ] |
[1388] | Philip Wadler. The essence of functional programming. In Principles of Programming Languages (POPL), pages 1--14, 1992. Invited talk. [ bib | .ps ] |
[1389] | Philip Wadler. The Girard-Reynolds isomorphism (second edition). Theoretical Computer Science, 375(1--3):201--226, May 2007. [ bib | .pdf ] |
[1390] | Philip Wadler and Stephen Blott. How to make ad-hoc polymorphism less ad-hoc. In Principles of Programming Languages (POPL), pages 60--76, January 1989. [ bib | .ps.gz ] |
[1391] | 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 ] |
[1392] | Philip L. Wadler. How to replace failure by a list of successes. In Functional Programming Languages and Computer Architecture (FPCA), volume 201 of Lecture Notes in Computer Science, pages 113--128. Springer, September 1985. [ bib | http ] |
[1393] | David Walker. A type system for expressive security policies. In Principles of Programming Languages (POPL), pages 254--267, January 2000. [ bib | http ] |
[1394] | 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 ] |
[1395] | David Walker, Karl Crary, and Greg Morrisett. Typed memory management via static capabilities. ACM Transactions on Programming Languages and Systems, 22(4):701--771, 2000. [ bib | .pdf ] |
[1396] | David Walker and Greg Morrisett. Alias types for recursive data structures. In Types in Compilation (TIC), volume 2071 of Lecture Notes in Computer Science, pages 177--206. Springer, September 2000. [ bib | .pdf ] |
[1397] | Dan S. Wallach. A new approach to mobile code security. PhD thesis, Princeton University, January 1999. [ bib | .html ] |
[1398] | 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 ] |
[1399] | Dan S. Wallach and Edward Felten. Understanding Java stack inspection. In IEEE Symposium on Security and Privacy (S&P), May 1998. [ bib | http ] |
[1400] | Mitchell Wand. Continuation-based program transformation strategies. Journal of the ACM, 27(1):164--180, 1980. [ bib | http ] |
[1401] | Mitchell Wand. Embedding type structure in semantics. In Principles of Programming Languages (POPL), pages 1--6, January 1985. [ bib | http ] |
[1402] | Mitchell Wand. Finding the source of type errors. In Principles of Programming Languages (POPL), pages 38--43, January 1986. [ bib | http ] |
[1403] | Mitchell Wand. A simple algorithm and proof for type inference. Fundamenta Informaticæ, 10:115--122, 1987. [ bib | .pdf ] |
[1404] | Mitchell Wand. Correctness of procedure representations in higher-order assembly language. In Mathematical Foundations of Programming Semantics, volume 598 of Lecture Notes in Computer Science, pages 294--311. Springer, March 1991. [ bib | .dvi ] |
[1405] | Mitchell Wand. Type inference for record concatenation and multiple inheritance. Information and Computation, 93(1):1--15, July 1991. [ bib | .dvi ] |
[1406] | 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 ] |
[1407] | Mitchell Wand and Paul A. Steckler. Selective and lightweight closure conversion. In Principles of Programming Languages (POPL), pages 435--445, January 1994. [ bib | http ] |
[1408] | Peng Wang, Di Wang, and Adam Chlipala. TiML: A functional language for practical complexity analysis with invariants. Proceedings of the ACM on Programming Languages, 1(OOPSLA):79:1--79:26, October 2017. [ bib | .pdf ] |
[1409] | 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 ] |
[1410] | 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 ] |
[1411] | Alessandro Warth, James R. Douglass, and Todd D. Millstein. Packrat parsers can support left recursion. In ACM Workshop on Evaluation and Semantics-Based Program Manipulation (PEPM), pages 103--110, January 2008. [ bib | .pdf ] |
[1412] | Ben Wegbreit. Mechanical program analysis. Communications of the ACM, 18(9):528--539, September 1975. [ bib | http ] |
[1413] | Ingo Wegener. A simplified correctness proof for a well-known algorithm computing strongly connected components. Information Processing Letters, 83(1):17--19, 2002. [ bib | .pdf ] |
[1414] | Stephanie Weirich. Type-safe cast: Functional pearl. In International Conference on Functional Programming (ICFP), pages 58--67, September 2000. [ bib | .pdf ] |
[1415] | 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 ] |
[1416] | Stephanie Weirich. RepLib: a library for derivable type classes. In Haskell workshop, pages 1--12, 2006. [ bib | .pdf ] |
[1417] | Stephanie Weirich. Type-safe run-time polytypic programming. Journal of Functional Programming, 16(10):681--710, November 2006. [ bib | .pdf ] |
[1418] | Stephanie Weirich, Brent A. Yorgey, and Tim Sheard. Binders unbound. In International Conference on Functional Programming (ICFP), pages 333--345, September 2011. [ bib | .pdf ] |
[1419] | J. B. Wells. The undecidability of Mitchell's subtyping relation. Technical Report 95-019, Computer Science Department, Boston University, December 1995. [ bib | .ps.gz ] |
[1420] | 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 ] |
[1421] | 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, 2002. [ bib | .pdf ] |
[1422] | Benjamin Werner. Une théorie des constructions inductives. PhD thesis, Université Paris 7, 1994. [ bib ] |
[1423] | Edwin Westbrook, Aaron Stump, and Ian Wehrman. A language-based approach to functionally correct imperative programming. In International Conference on Functional Programming (ICFP), pages 268--279, 2005. [ bib | .pdf ] |
[1424] | Edwin M. Westbrook. Higher-order encodings with constructors. PhD thesis, Washington University, December 2008. [ bib | .pdf ] |
[1425] | J. W. J. Williams. Algorithm 232: Heapsort. Communications of the ACM, 7(6):347--348, June 1964. [ bib | http ] |
[1426] | Simon Wimmer, Shuwei Hu, and Tobias Nipkow. Verified memoization and dynamic programming. In Interactive Theorem Proving (ITP), volume 10895 of Lecture Notes in Computer Science, pages 579--596. Springer, July 2018. [ bib | .pdf ] |
[1427] | 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 ] |
[1428] | Niklaus Wirth. Algorithms + data structures = programs. Prentice Hall, 1978. [ bib ] |
[1429] | Ryan Wisnesky, Gregory Malecha, and Greg Morrisett. Certified web services in Ynot. In Workshop on Automated Specification and Verification of Web Systems, July 2009. [ bib | .pdf ] |
[1430] | Roger Wolff, Ronald Garcia, Éric Tanter, and Jonathan Aldrich. Gradual typestate. In European Conference on Object-Oriented Programming (ECOOP), volume 6813 of Lecture Notes in Computer Science, pages 459--483. Springer, July 2011. [ bib | .pdf ] |
[1431] | J. P. L. Woodward. Applications for multilevel secure operating systems. In Proceedings NCC, volume 48, pages 319--328. AFIPS Press, June 1979. [ bib ] |
[1432] | Andrew K. Wright. Polymorphism for imperative languages without imperative types. Technical Report 93-200, Rice University, February 1993. [ bib ] |
[1433] | Andrew K. Wright. Simple imperative polymorphism. Lisp and Symbolic Computation, 8(4):343--356, December 1995. [ bib | .ps.gz ] |
[1434] | 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 ] |
[1435] | Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38--94, November 1994. [ bib | .ps.gz ] |
[1436] | Hongwei Xi. Dependent types in practical programming. PhD thesis, Carnegie Mellon University, December 1998. [ bib | .ps ] |
[1437] | Hongwei Xi. Dead code elimination through dependent types. In Practical Aspects of Declarative Languages (PADL), volume 1551 of Lecture Notes in Computer Science, pages 228--242. Springer, January 1999. [ bib | .ps ] |
[1438] | Hongwei Xi. Dependent ML, 2001. [ bib | .html ] |
[1439] | Hongwei Xi. Dependently Typed Pattern Matching. Journal of Universal Computer Science, 9(8):851--872, 2003. [ bib | .pdf ] |
[1440] | Hongwei Xi. Applied type system. In TYPES 2003, volume 3085 of Lecture Notes in Computer Science, pages 394--408. Springer, February 2004. [ bib | .pdf ] |
[1441] | Hongwei Xi. Dependent ML: an approach to practical programming with dependent types. Journal of Functional Programming, 17(2):215--286, 2007. [ bib | .pdf ] |
[1442] | Hongwei Xi, Chiyan Chen, and Gang Chen. Guarded recursive datatype constructors. In Principles of Programming Languages (POPL), pages 224--235, January 2003. [ bib | .ps ] |
[1443] | Hongwei Xi and Frank Pfenning. Dependent types in practical programming. In Principles of Programming Languages (POPL), pages 214--227, January 1999. [ bib | .ps ] |
[1444] | Hongwei Xi and Carsten Schürmann. CPS transform for Dependent ML. In Workshop on Logic, Language, Information and Computation (WoLLIC), August 2001. [ bib | .pdf ] |
[1445] | Yichen Xie and Alex Aiken. Scalable error detection using Boolean satisfiability. In Principles of Programming Languages (POPL), pages 351--363, January 2005. [ bib | .pdf ] |
[1446] | Dana N. Xu. Extended static checking for Haskell. In Haskell workshop, pages 48--59. ACM Press, 2006. [ bib | .ps ] |
[1447] | Dana N. Xu, Simon Peyton Jones, and Koen Claessen. Static contract checking for Haskell. In Principles of Programming Languages (POPL), pages 41--52, January 2009. [ bib | .ps ] |
[1448] | Jeremy Yallop. Staged generic programming. Proceedings of the ACM on Programming Languages, 1(ICFP):29:1--29:29, 2017. [ bib | .pdf ] |
[1449] | Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, and Peter W. O'Hearn. Scalable shape analysis for systems code. In Computer Aided Verification (CAV), volume 5123 of Lecture Notes in Computer Science, pages 385--398. Springer, July 2008. [ bib | .pdf ] |
[1450] | Kwangkeun Yi. Educational pearl: 'proof-directed debugging' revisited for a first-order version. Journal of Functional Programming, 16(6):663--670, 2006. [ bib | .pdf ] |
[1451] | Nobuko Yoshida. Graph types for monadic mobile processes. In Foundations of Software Technology and Theoretical Computer Science (FSTTCS), volume 1180 of Lecture Notes in Computer Science, pages 371--386. Springer, 1996. [ bib | .ps.gz ] |
[1452] | Nobuko Yoshida. Graph types for monadic mobile processes. Technical Report ECS-LFCS-96-350, University of Edinburgh, 1996. [ bib | http ] |
[1453] | Nobuko Yoshida, Kohei Honda, and Martin Berger. Linearity and bisimulation. Technical Report MSC-2001/48, University of Leicester, December 2001. [ bib | .ps.gz ] |
[1454] | Nobuko Yoshida, Kohei Honda, and Martin Berger. Linearity and bisimulation. In Foundations of Software Science and Computation Structures (FOSSACS), Lecture Notes in Computer Science. Springer, April 2002. [ bib | .ps.gz ] |
[1455] | Nobuko Yoshida, Kohei Honda, and Martin Berger. Logical reasoning for higher-order functions with local state. In Foundations of Software Science and Computation Structures (FOSSACS), volume 4423 of Lecture Notes in Computer Science, pages 361--377. Springer, April 2007. [ bib | .pdf ] |
[1456] | Steve Zdancewic and Andrew C. Myers. Secure information flow and CPS. In European Symposium on Programming (ESOP), Lecture Notes in Computer Science. Springer, April 2001. [ bib | .ps ] |
[1457] | 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 ] |
[1458] | Olivier Zendra, Dominique Colnet, and Suzanne Collin. Efficient dynamic dispatch without virtual function tables. the SmallEiffel compiler. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 125--141, October 1997. [ bib | .ps.gz ] |
[1459] | Christoph Zenger. Indexed types. Theoretical Computer Science, 187(1--2):147--165, 1997. [ bib | http ] |
[1460] | Christoph Zenger. Indizierte typen. PhD thesis, Universität Karlsruhe, July 1998. [ bib | .ps.gz ] |
[1461] | Bohua Zhan and Maximilian P. L. Haslbeck. Verifying asymptotic time complexity of imperative programs in Isabelle. In International Joint Conference on Automated Reasoning, July 2018. [ bib | http ] |
[1462] | Hongbo Zhang and Steve Zdancewic. Fan: compile-time metaprogramming for OCaml. Unpublished, March 2013. [ bib | .pdf ] |
[1463] | Yizhou Zhang and Andrew C. Myers. Abstraction-safe effect handlers via tunneling. Proceedings of the ACM on Programming Languages, 3(POPL):5:1--5:29, 2019. [ bib | .pdf ] |
[1464] | Yang Zhao. Concurrency analysis based on fractional permission system. PhD thesis, University of Wisconsin, August 2007. [ bib | .pdf ] |
[1465] | Lantian Zheng and Andrew C. Myers. Dynamic security labels and noninterference. Technical Report 2004-1924, Cornell University, January 2004. [ bib | .pdf ] |
[1466] | 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, November 2003. [ bib | .pdf ] |
[1467] | Dengping Zhu and Hongwei Xi. Safe programming with pointers through stateful views. In Practical Aspects of Declarative Languages (PADL), volume 3350 of Lecture Notes in Computer Science, pages 83--97. Springer, January 2005. [ bib | .pdf ] |
[1468] | Yoav Zibin and Yossi Gil. Theory and practice of incremental subtyping tests and message dispatching, December 2001. [ bib | .ps.gz ] |
[1469] | Yoav Zibin and Yossi Gil. Fast algorithm for creating space efficient dispatching tables with application to multi-dispatching. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 142--160, November 2002. [ bib | .pdf ] |
[1470] | Yoav Zibin and Yossi Gil. Incremental algorithms for dispatching in dynamically typed languages. In Principles of Programming Languages (POPL), January 2003. [ bib | .pdf ] |
[1471] | Jan Zwanenburg. A type system for record concatenation and subtyping. Technical report, Eindhoven University of Technology, July 1997. [ bib | .ps ] |
This file was generated by bibtex2html 1.99.