Dependent types and program equivalence. (English) Zbl 1312.68062
Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’10, Madrid, Spain, January 17–23, 2010. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-60558-479-9). 275-286 (2010).
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68N15 | Theory of programming languages |
References:
| [1] | Thorsten Altenkirch and Nicolas Oury. PiSigma: A core language for dependently typed programming. Draft, 2008. |
| [2] | Lennart Augustsson. Cayenne-a language with dependent types. In Proc. 3rd ACM Symp. on Principles of Programming Languages (ICFP), pages 239-250, 1998. 10.1145/289423.289451 · Zbl 1428.68094 |
| [3] | Brian Aydemir and Stephanie Weirich. LNgen: Tool support for locally nameless representations. Submitted for publication, October 2009. |
| [4] | H. P. Barendregt. The lambda calculus: Its syntax and semantics. North-Holland Pub. Co., 1981. · Zbl 0467.03010 |
| [5] | Bruno Barras and Bruno Bernardo. The Implicit Calculus of Constructions as a programming language with dependent types. In Proc. of the 11th International Conf. on Foundations of Software Science and Computational Structures (FoSSaCS), pages 365-379, 2008. · Zbl 1138.68356 |
| [6] | Luca Cardelli. Apolymorphic lambda-calculus with type:type. Technical Report SRC Research Report 10, Digital Equipment Corporation Systems Research Center, May 1986. |
| [7] | The Coq Development Team. The Coq Proof Assistant Reference Manual (Version 8.2), 2009. URL http://coq.inria.fr. |
| [8] | Thierry Coquand. An algorithm for testing conversion in Type Theory. In Gérard Huet and Gordon Plotkin, editors, Logical Frameworks, pages 255-277, 1991. · Zbl 0754.03041 |
| [9] | Seth Fogarty, Emir Pasalic, Jeremy Siek, andWalid Taha. Concoqtion: indexed types now! In ACM SIGPLAN 2007 Workshop on Partial Evaluation and Program Manipulation (PEPM), pages 112-121, 2007. 10.1145/1244381.1244400 |
| [10] | Jean-Yves Girard. Interprétation fonctionelle et élimination des coupures de l’arithmétique d’ordre supérieur. PhD thesis, Université Paris VII, 1972. |
| [11] | Mark P. Jones. A system of Constructor Classes: Overloading and implicit higher-order polymorphism. J. Funct. Program., 5(1):1-35, 1995. · Zbl 0819.68027 |
| [12] | Xavier Leroy. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In Proc. 33rd ACM Symp. on Principles of Programming Languages (POPL), pages 42-54, 2006. 10.1145/1111037.1111042 · Zbl 1369.68124 |
| [13] | Daniel R. Licata and Robert Harper. A formulation of Dependent ML with explicit equality proofs. Technical Report CMU-CS-05-178, Carnegie Mellon University Dept. of Computer Science, 2005. |
| [14] | Ian A. Mason and Carolyn L. Talcott. Equivalence in Functional Languages with Effects. J. Funct. Program., 1(3):287-327, 1991. · Zbl 0941.68540 |
| [15] | C McBride and J McKinna. The view from the left. J. Funct. Program., 14(1):69-111, 2004. 10.1017/S0956796803004829 · Zbl 1069.68539 |
| [16] | Nathan Mishra-Linger and Tim Sheard. Erasure and polymorphism in Pure Type Systems. In Proc. of the 11th International Conf. on Foundations of Software Science and Computational Structures (FoSSaCS), pages 350-364, 2008. · Zbl 1138.68361 |
| [17] | Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, and Lars Birkedal. Ynot: dependent types for imperative programs. In Proc. 13th ACM Symp. on Principles of Programming Languages (ICFP), pages 229-240, 2008. 10.1145/1411204.1411237 · Zbl 1323.68142 |
| [18] | Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University, 2007. |
| [19] | Xinming Ou, Gang Tan, Yitzhak Mandelbaum, and David Walker. Dynamic typing with dependent types. In IFIP International Conference on Theoretical Computer Science, pages 437-450, 2004. · Zbl 1088.68531 |
| [20] | Nicolas Oury and Wouter Swierstra. The power of Pi. In Proc. 13th ACM Symp. on Principles of Programming Languages (ICFP), pages 39-50, 2008. 10.1145/1411204.1411213 · Zbl 1323.68145 |
| [21] | Simon L. Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. Simple unification-based type inference for GADTs. In Proc. 11th ACM Symp. on Principles of Programming Languages (ICFP), pages 50-61, 2006. 10.1145/1159803.1159811 |
| [22] | Adam Poswolsky and Carsten Schürmann. Practical programming with higher-order encodings and dependent types. In Proc. of the 17th European Symp. on Programming (ESOP), pages 93-107, 2008. · Zbl 1133.68312 |
| [23] | François Pottier and Yann Régis-Gianas. Stratified type inference for generalized algebraic data types. In Proc. 33rd ACM Symp. on Principles of Programming Languages (POPL), pages 232-244, 2006. 10.1145/1111037.1111058 · Zbl 1369.68114 |
| [24] | Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and Rok Strniša. Ott: Effective Tool Support for the Working Semanticist. In Proc. 12th ACM Symp. on Principles of Programming Languages (ICFP), pages 1-12, 2007. 10.1145/1291151.1291155 · Zbl 1291.68238 |
| [25] | T. Sheard. Type-level computation using narrowing in ©omega. In The 1st workshop on Programming Languages meets Program Verification (PLPV), pages 105-128, 2006. · Zbl 1277.68046 |
| [26] | Chris Stone and Robert Harper. Deciding type equivalence in a language with singleton kinds. In Proc. 27th ACM Symp. on Principles of Programming Languages (POPL), pages 214-227, 2000. 10.1145/325694.325724 · Zbl 1323.68163 |
| [27] | Aaron Stump, Morgan Deters, Adam Petcher, Todd Schiller, and Timothy Simpson. Verified programming in Guru. In Proc. of the 3rd workshop on Programming Languages meets Program Verification (PLPV), pages 49-58, 2009. 10.1145/1481848.1481856 |
| [28] | Dimitrios Vytiniotis and Stephanie Weirich. Dependent types: Easy as PIE. In 8th Symp. on Trends in Functional Programming, 2007. |
| [29] | Joe 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. · Zbl 0932.03017 |
| [30] | Andrew K. Wright and Matthias Felleisen. A Syntactic Approach to Type Soundness. Information and Computation, 115:38-94, 1994. 10.1006/inco.1994.1093 · Zbl 0938.68559 |
| [31] | Hongwei Xi. Applied type system. In Proceedings of TYPES 2003, Lecture Notes in Computer Science, pages 394-408. 2004. · Zbl 1100.03518 |
| [32] | Hongwei Xi and Frank Pfenning. Dependent types in practical programming. In Proc. 26th ACM Symp. on Principles of Programming Languages (POPL), pages 214-227, 1999. 10.1145/292540.292560 |
| [33] | Hongwei Xi, Chiyan Chen, and Gang Chen. Guarded recursive datatype constructors. In Proc. 30th ACM Symp. on Principles of Programming Languages (POPL), pages 224-235, 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.
