A foundation for flow-based program matching: using temporal logic and model checking. (English) Zbl 1315.68176
Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’09, Savannah, GA, USA, January 18–24, 2009. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-60558-379-2). 114-126 (2009).
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
References:
| [1] | Ki Yung Ahn and Tim Sheard. Shared subtypes: subtyping recursive parametrized algebraic data types. In Haskell ’08: Proceedings of the 1st ACM SIGPLAN Haskell symposium, pages 75-86, New York, NY, USA, 2008. ACM. 10.1145/1411286.1411297 |
| [2] | James Cheney and Ralf Hinze. First-class phantom types. Technical Report CUCIS TR2003-1901, Cornell University, 2003. |
| [3] | Dominic Duggan and John Ophel. Type-checking multi-parameter type classes. J. Funct. Program., 12 (2): 133-158, 2002. 10.1017/S0956796801004233 · Zbl 0994.68034 |
| [4] | Louis-Julien Guillemette and Stefan Monnier. A type-preserving compiler in Haskell. In ICFP ’08: Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, pages 75-86, New York, NY, USA, 2008. ACM. 10.1145/1411204.1411218 · Zbl 1323.68187 |
| [5] | Mark P. Jones. Type classes with functional dependencies. In Proc. of ESOP 2000, number 1782 in Lecture Notes in Computer Science. Springer-Verlag, 2000. · Zbl 0971.68641 |
| [6] | Christine Paulin-Mohring. Inductive definitions in the system Coq-rules and properties. In M. Bezem and J. Groote, editors, International conference on Typed Lambda Calculi and Applications. LNCS 664, Springer-Verlag, 1993. |
| [7] | Simon Peyton Jones, Mark P. Jones, and Erik Meijer. Type classes: exploring the design space. In Haskell Workshop, Amsterdam, June 1997. |
| [8] | Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. Simple unification-based type inference for gadts. In International Conference on Functional Programming, Portland, Oregon, September 2006. 10.1145/1159803.1159811 |
| [9] | Frank Pfenning and Carsten Schürmann. System description: Twelf – a meta-logical framework for deductive systems. In International Conference on Automated Deduction, volume 1632 of Lecture Notes in Artificial Intelligence, pages 202-206, July 1999. |
| [10] | Tom Schrijvers and Martin Sulzmann. Unified Type Checking for Type Classes and Type Functions, 2008. Poster at the International Conference on Functional Programming (ICFP’08). |
| [11] | Tom Schrijvers, Simon Peyton Jones, Manuel Chakravarty, and Martin Sulzmann. Type checking with open type functions. In ICFP ’08: Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, pages 51-62, New York, NY, USA, 2008. ACM. 10.1145/1411204.1411215 · Zbl 1323.68156 |
| [12] | Tim Sheard. Languages of the future. In OOPSLA ’04: Companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, pages 116-119, New York, NY, USA, 2004. ACM Press. ISBN 1-58113-833-4. 10.1145/1028664.1028711 |
| [13] | Matthieu Sozeau and Nicolas Oury. First-class type classes. In 21th International Conference on Theorem Proving in Higher Order Logics, pages 278-293. LNCS 5170, Springer-Verlag, 2008. 10.1007/978-3-540-71067-7_23 · Zbl 1165.68475 |
| [14] | Peter J. Stuckey and Martin Sulzmann. A theory of overloading. ACM Transactions on Programming Languages and Systems (TOPLAS), 27 (6): 1-54, 2005. 10.1145/1108970.1108974 |
| [15] | Martin Sulzmann, Manuel Chakravarty, Simon Peyton Jones, and Kevin Donnelly. System F with type equality coercions. In ACM SIGPLAN International Workshop on Types in Language Design and Implementation (TLDI’07). ACM, 2007. 10.1145/1190315.1190324 |
| [16] | Martin Sulzmann, Gregory J. Duck, Simon Peyton-Jones, and Peter J. Stuckey. Understanding functional dependencies via Constraint Handling Rules. J. Funct. Program., 17 (1): 83-129, 2007. 10.1017/S0956796806006137 · Zbl 1107.68031 |
| [17] | Philip Wadler and Stephen Blott. How to make ad-hoc polymorphism less ad hoc. In Symposium on Principles of Programming Languages, Austin, TX, January 1989. 10.1145/75277.75283 |
| [18] | Hongwei Xi, Chiyan Chen, and Gang Chen. Guarded recursive datatype constructors. In Symposium on Principles of Programming Languages, pages 224-235, New Orleans, LA, January 2003. 10.1145/604131.604150 · Zbl 1321.68161 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
