A New Approach to Abstract Syntax with Variable Binding
Tóm tắt
The permutation model of set theory with atoms (FM-sets), devised by Fraenkel and Mostowski in the 1930s, supports notions of ‘name-abstraction’ and ‘fresh name’ that provide a new way to represent, compute with, and reason about the syntax of formal systems involving variable-binding operations. Inductively defined FM-sets involving the name-abstraction set former (together with Cartesian product and disjoint union) can correctly encode syntax modulo renaming of bound variables. In this way, the standard theory of algebraic data types can be extended to encompass signatures involving binding operators. In particular, there is an associated notion of structural recursion for defining syntax-manipulating functions (such as capture avoiding substitution, set of free variables, etc.) and a notion of proof by structural induction, both of which remain pleasingly close to informal practice in computer science.
Từ khóa
Tài liệu tham khảo
Abadi M., 1999, A calculus for cryptographic protocols: the spi calculus, Information and Computation, 148, 1, 10.1006/inco.1998.2740
Barendregt H. P., 1984, North-Holland
Burstall R. M., 1969, Proving properties of programs by structural induction, Computer Journal, 12, 41, 10.1093/comjnl/12.1.41
Burstall R. M., 1977, Proceedings of the Infotech State of the Art Conference
Cardelli L., 2001, 5th International Conference, 2044
Cardelli L., 2000, Mobile ambients, Theoretical Computer Science, 240, 177, 10.1016/S0304-3975(99)00231-5
Church A., 1940, A formulation of the simple theory of types, Journal of Symbolic Logic, 5, 56, 10.2307/2266170
Curien P.-L., 1993, Sequential Algorithms, and Functional Programming
de Bruijn N. G., 1972, Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem, Indag. Math., 34, 381, 10.1016/1385-7258(72)90034-0
Despeyroux J., 2000, IFIP International Conference on Theoretical Computer Science, IFIP TCS'2000
Despeyroux J., 1997, 3rd International Conference, 1210, 147
Fiore M. P., 1996, Eleventh Annual Symposium on Logic in Computer Science, IEEE Computer Society Press, 43
Fiore M. P., 1999, 14th Annual Symposium on Logic in Computer Science, IEEE Computer Society Press, 193
Fourman M. P., 1980, Sheaf models for set theory, Journal of Pure and Applied Algebra, 19, 91, 10.1016/0022-4049(80)90096-1
Gordon M. J. C., 1993, Introduction to HOL. A theorem proving environment for higher order logic
Gordon A. D., 1996, Theorem Proving in Higher Order Logics: 9th Interational Conference, TPHOLs'96, 1125, 173, 10.1007/BFb0105404
Gabbay M. J., 1999, 14th Annual Symposium on Logic in Computer Science, IEEE Computer Society Press, 214
Goguen J. A., 1977, Initial algebra semantics and continuous algebras, JACM, 24, 68, 10.1145/321992.321997
Gunter C. A., 1992, : Semantics of Programming Languages: Structures and Techniques. Foundations of Computing
Honsell F., 1998, Dipartimento di Matematica e Informatica, Università degli Studi di Udine
Hofmann M., 1999, 14th Annual Symposium on Logic in Computer Science, IEEE Computer Society Press, 204
Honda K., 2000, Elementary structures in process theory (1): Sets with renaming, Mathematical Structures in Computer Science, 10, 617, 10.1017/S0960129599002947
Joyal A., 1995, Algebraic Set Theory. Number 220 in London Mathematical Society Lecture Notes in Mathematics
Johnstone P. T., 1983, Quotients of decidable objects in a topos, Mathematical Proceedings of Cambridge Philosophical Society, 93, 409, 10.1017/S0305004100060734
Jeffrey A., 1999, 14th Annual Symposium on Logic in Computer Science, IEEE Computer Society Press, 56
Lamport L., 1999, Should your specification language be typed?, ACM Transactions on Programming Languages and Systems, 21, 502, 10.1145/319301.319317
Lambek J., 1986, Introduction to Higher Order Categorical Logic
Martin-Löf P., 1984, Bibliopolis
MacLane S., 1992, Sheaves in Geometry and Logic: A First Introduction to Topos Theory
McDowell R., 1997, 12th Annual Symposium on Logic in Computer Science, IEEE Computer Society Press, 434
Montanari U., 2000, 25th International Symposium on Mathematical Foundations of Computer Science, Bratislava, Slovak Republic, 1893
Milner R., 1992, A calculus of mobile processes (parts I and II), Information and Computation, 100, 1, 10.1016/0890-5401(92)90008-4
Pfenning F., 1988, Proceedings of ACM-SIGPLAN Conference on Programming Language Design and Implementation, ACM Press, 199
Pitts A. M., 2000, Mathematics of Program Construction: 5th International Conference, MPC2000, 230, 10.1007/10722010_15
[PaM93] Paulin-Mohring C. : Inductive definitions in the system Coq ; rules and properties. In M. Bezem and J. F. Groote editors Typed Lambda Calculus and Applications Vol. 664 of Lecture Notes in Computer Science Springer Berlin 1993 pp. 328 - 345 .
Pitts A. M., 1993, Proceedings of the 18th International Symposium, Gdańsk., 711, 122
Pitts A. M., 1993, Workshop on State in Programming Languages, 31
Reynolds J. C., 1983, Information Processing 83, 513
Scott D. S., 1993, A type-theoretical alternative to ISWIM, CUCH, OWHY. Theoretical Computer Science, 121, 411, 10.1016/0304-3975(93)90095-B
Stark I. D. B., 1996, Categorical models for local names, Lisp and Symbolic Computation, 9, 77, 10.1007/BF01806033
Stark I. D. B., 1996, 11th Annual Symposium on Logic in Computer Science, IEEE Computer Society Press, 36