Programming with binders and indexed data-types. (English) Zbl 1321.68141
Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’12, Philadelphia, PA, USA, January 22–28, 2012. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-1083-3). 413-424 (2012).
MSC:
| 68N18 | Functional programming and lambda calculus |
| 68N15 | Theory of programming languages |
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
References:
| [1] | Martın Abadi, Michael Burrows, Butler W. Lampson, and Gordon D. Plotkin. A calculus for access control in distributed systems. ACM Transaction on Programming Language Systems, 15 (4): 706-734, 1993. 10.1145/155183.155225 |
| [2] | Martin Abadi, Anindya Banerjee, Nevin Heintze, and Jon G. Riecke. A core calculus of dependency. In 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’99), pages 147-160. ACM Press, 1999. 10.1145/292540.292555 |
| [3] | Andreas Abel. Mixed inductive/coinductive types and strong normalization. In Zhong Shao, editor, ph5th ASIAN Symposium on Programming Languages and Systems (APLAS’07), volume 4807 of Lecture Notes in Computer Science, pages 286-301. Springer, 2007. · Zbl 1138.68023 |
| [4] | Andreas Abel. Polarized subtyping for sized types. Mathematical Structures in Computer Science, 18 (5): 797-822, 2008. Special issue on subtyping, edited by Healfdene Goguen and Adriana Compagnoni. · Zbl 1156.68014 |
| [5] | David Baelde, Zach Snow, and Dale Miller. Focused inductive theorem proving. In Jürgen Giesl and Reiner Haehnle, editors, 5th International Joint Conference on Automated Reasoning (IJCAR’10), Lecture Notes in Artificial Intelligence (LNAI 6173), pages 278-292. Springer, 2010. 10.1007/978-3-642-14203-1_24 · Zbl 1291.68322 |
| [6] | Ulrich Berger and Helmut Schwichtenberg. An inverse of the evaluation functional for typed lambda-calculus. In Logic in Computer Science, pages 203-211, 1991. |
| [7] | Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Springer, 2004. · Zbl 1069.68095 |
| [8] | Chiyan Chen and Hongwei Xi. Combining programming with theorem proving. In Olivier Danvy and Benjamin C. Pierce, editors, ph10th International Conference on Functional Programming, pages 66-77, 2005. 10.1145/1086365.1086375 · Zbl 1302.68241 |
| [9] | Patrick Cousot and Radhia Cousot. Inductive definitions, semantics and abstract interpretations. In 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’92), pages 83-94. ACM, 1992. 10.1145/143165.143184 |
| [10] | Kevin Donnelly and Hongwei Xi. Combining higher-order abstract syntax with first-order abstract syntax in ats. In Randy Pollack, editor, Workshop on Mechanized Reasoning about Languages with Variable Binding (MERLIN’05), pages 58-63. ACM, 2005. 10.1145/1088454.1088462 |
| [11] | Joshua Dunfield and Brigitte Pientka. Case analysis of higher-order data. In International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP’08), volume 228 of Electronic Notes in Theoretical Computer Science (ENTCS), pages 69-84. Elsevier, June 2009. 10.1016/j.entcs.2008.12.117 · Zbl 1337.68058 |
| [12] | Andrew Gacek, Dale Miller, and Gopalan Nadathur. Combining generic judgments with recursive definitions. In F. Pfenning, editor, 23rd Symposium on Logic in Computer Science. IEEE Computer Society Press, 2008. 10.1109/LICS.2008.33 |
| [13] | D. Garg and F. Pfenning. Non-interference in constructive authorization logic. In Proceedings of the 19th IEEE Computer Security Foundations Workshop (CSFW 19). IEEE Computer Society Press, 2006. 10.1109/CSFW.2006.18 |
| [14] | Louis-Julien Guillemette and Stefan Monnier. A type-preserving closure conversion in Haskell. In Proceedings of the ACM SIGPLAN Workshop on Haskell, Haskell ’07, pages 83-92, 2007. 10.1145/1291201.1291212 |
| [15] | Robert Harper and Daniel R. Licata. Mechanizing Metatheory in a Logical Framework. Journal of Functional Programming, 17 (4-5): 613-673, 2007. 10.1017/S0956796807006430 · Zbl 1125.68029 |
| [16] | Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40 (1): 143-184, January 1993. 10.1145/138027.138060 · Zbl 0778.03004 |
| [17] | Xavier Leroy and Hervé Grall. Coinductive big-step operational semantics. Information and Computation, pages 284-304, 2009. 10.1016/j.ic.2007.12.004 · Zbl 1165.68044 |
| [18] | Daniel R. Licata. Dependently Typed Programming with Domain-Specific Logics. PhD thesis, Carnegie Mellon University, 2011. |
| [19] | Daniel R. Licata and Robert Harper. A universe of binding and computation. In Graham Hutton and Andrew P. Tolmach, editors, 14th ACM SIGPLAN International Conference on Functional Programming, pages 123-134. ACM Press, 2009. 10.1145/1596550.1596571 · Zbl 1302.68050 |
| [20] | Daniel R. Licata, Noam Zeilberger, and Robert Harper. Focusing on binding and computation. In F. Pfenning, editor, 23rd Symposium on Logic in Computer Science, pages 241-252. IEEE Computer Society Press, 2008. 10.1109/LICS.2008.48 |
| [21] | Raymond C. McDowell and Dale A. Miller. Reasoning with higher-order abstract syntax in a logical framework. ACM Transactions on Computational Logic, 3 (1): 80-136, 2002. ISSN 1529-3785. 10.1145/504077.504080 · Zbl 1365.68164 |
| [22] | Yasuhiko Minamide, Greg Morrisett, and Robert Harper. Typed closure conversion. In Twenty-Third ACM Symposium on Principles of Programming Languages, pages 271-283. ACM Press, 1996. 10.1145/237721.237791 |
| [23] | Kenji Miyamoto and Atsushi Igarashi. A modal foundation for secure information flow. In A. Sabelfeld, editor, Workshop on Foundations of Computer Security (FCS’04), pages 187-203, 2004. |
| [24] | Aleksandar Nanevski, J. Gregory Morrisett, and Lars Birkedal. Hoare type theory, polymorphism and separation. Journal of Functional Programming, 18 (5-6): 865-911, 2008. 10.1017/S0956796808006953 · Zbl 1155.68354 |
| [25] | Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. Contextual modal type theory. ACM Transactions on Computational Logic, 9 (3): 1-49, 2008. 10.1145/1352582.1352591 · Zbl 1367.03060 |
| [26] | Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, September 2007. Technical Report 33D. |
| [27] | Christine Paulin-Mohring. Inductive definitions in the system coq - rules and properties. In Marc Bezem and Jan Friso Groote, editors, International Conference on Typed Lambda Calculi and Applications(TLCA ’93), volume 664 of Lecture Notes in Computer Science, pages 328-345. Springer, 1993. · Zbl 0844.68073 |
| [28] | Frank Pfenning and Carsten Schürmann. System description: Twelf – a meta-logical framework for deductive systems. In H. Ganzinger, editor, ph16th International Conference on Automated Deduction (CADE-16), volume 1632 of Lecture Notes in Artificial Intelligence, pages 202-206. Springer, 1999. |
| [29] | Brigitte Pientka. A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’08), pages 371-382. ACM Press, 2008. 10.1145/1328438.1328483 · Zbl 1295.68068 |
| [30] | Brigitte Pientka. Programming proofs: A novel approach based on contextual types. submitted, 2011. |
| [31] | Brigitte Pientka and Joshua Dunfield. Beluga: a framework for programming and reasoning with deductive systems (System Description). In Jürgen Giesl and Reiner Haehnle, editors, 5th International Joint Conference on Automated Reasoning (IJCAR’10), Lecture Notes in Artificial Intelligence (LNAI 6173), pages 15-21. Springer-Verlag, 2010. 10.1007/978-3-642-14203-1_2 · Zbl 1291.68366 |
| [32] | ann(2009) |
| [33] | Adam B. Poswolsky and Carsten Schürmann. Practical programming with higher-order encodings and dependent types. In 17th European Symposium on Programming (ESOP ’08), volume 4960, pages 93-107. Springer, 2008. · Zbl 1133.68312 |
| [34] | François Pottier. Static name control for FreshML. In 22nd IEEE Symposium on Logic in Computer Science (LICS’07), pages 356-365. IEEE Computer Society, July 2007. 10.1109/LICS.2007.44 |
| [35] | Nicolas Pouillard and François Pottier. A fresh look at programming with names and binders. In 15th ACM SIGPLAN International Conference on Functional Programming (ICFP 2010), pages 217-228, 2010. 10.1145/1863543.1863575 · Zbl 1323.68082 |
| [36] | Susmit Sarkar. A Dependently Typed Programming Language, with applications to Foundational Certified Code Systems. PhD thesis, Carnegie Mellon University, 2009. Carnegie Mellon University-CS-09-128. |
| [37] | Carsten Schürmann and Frank Pfenning. A coverage checking algorithm for LF. In D. Basin and B. Wolff, editors, Proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs’03), pages 120-135. Springer, 2003. · Zbl 1279.68295 |
| [38] | Tim Sheard. Languages of the future. SIGPLAN Notices, 39 (12): 119-132, 2004. 10.1145/1052883.1052897 |
| [39] | Mark R. Shinwell, Andrew M. Pitts, and Murdoch J. Gabbay. FreshML: programming with binders made simple. In 8th International Conference on Functional Programming (ICFP’03), pages 263-274. ACM Press, 2003. 10.1145/944705.944729 · Zbl 1315.68058 |
| [40] | Antonis Stampoulis and Zhong Shao. VeriML: typed computation of logical terms inside a language with effects. In Paul Hudak and Stephanie Weirich, editors, 15th ACM SIGPLAN International Conference on Functional Programming (ICFP’10), pages 333-344. ACM, 2010. 10.1145/1863543.1863591 · Zbl 1323.68384 |
| [41] | Martin Sulzmann, Manuel M. T. Chakravarty, Simon Peyton Jones, and Kevin Donnelly. System f with type equality coercions. In ACM SIGPLAN International Workshop on Types in Languages Design and Implementation (TLDI’07), pages 53-66. ACM, 2007. 10.1145/1190315.1190324 |
| [42] | E. Westbrook, A. Stump, and I. Wehrman. A Language-based Approach to Functionally Correct Imperative Programming. In Olivier Danvy and Benjamin C. Pierce, editors, 10th International Conference on Functional Programming (ICFP05), pages 268-279. ACM, 2005. 10.1145/1086365.1086400 · Zbl 1302.68095 |
| [43] | Hongwei Xi. Applied type system. In phTYPES 2003, volume 3085 of Lecture Notes in Computer Science, pages 394-408. Springer, 2004. · Zbl 1100.03518 |
| [44] | Hongwei Xi and Frank Pfenning. Dependent types in practical programming. In 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’99), pages 214-227. ACM Press, 1999. 10.1145/292540.292560 |
| [45] | Hongwei Xi, Chiyan Chen, and Gang Chen. Guarded recursive datatype constructors. In 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’03), pages 224-235. ACM Press, 2003. 10.1145/604131.604150 · Zbl 1321.68161 |
| [46] | Christoph Zenger. Indexed types. Theoretical Computer Science, 187 (1-2): 147-165, 1997. 10.1016/S0304-3975(97)00062-5 · Zbl 0893.68086 |
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.
