Philip Wadler
Skip Abstract Section
Skip Supplemental Material SectionAbstract
Connecting mathematical logic and computation, it ensures that some aspects of programming are absolute.
Supplemental Material
Available for Download
pdf
p75-wadler-supp.pdf (247.8 KB)
Supplemental file.
- Abramsky, S. Computational interpretations of linear logic. Theoretical Compututer Science 111, 1--2 (1993), 3--57. Google Scholar
Digital Library
- Bates, J.L., Constable, R.L. Proofs as programs. Transactions on Programming Languages and Systems 7, 1 (Jan. 1985), 113--136. Google ScholarDigital Library
- Benton, P.N., Bierman, G.M., de Paiva, V. Computational types from a logical perspective. Journal of Functional Programming 8, 2 (1998), 177--193. Google ScholarDigital Library
- Caires, L., Pfenning, F. Session types as intuitionistic linear propositions. In Proceedings of the 21st International Conference on Concurrency Theory (Paris, France, Aug. 31--Sept. 3, 2010), 222--236. Google ScholarDigital Library
- Carroll, L. What the Tortoise said to Achilles. Mind 4, 14 (Apr. 1895), 278--280.Google Scholar
- Church, A. A set of postulates for the foundation of logic. Ann. Math. 33, 2 (1932), 346--366.Google ScholarCross Ref
- Church, A. An unsolvable problem of elementary number theory. American Journal of Mathematics 58, 2 (Apr. 1936), 345--363; presented to the American Mathematical Society, Apr. 19, 1935; abstract in Bulletin of the American Mathematical Society 41 (May 1935).Google ScholarCross Ref
- Church, A. A formulation of the simple theory of types. Journal of Symbolic Logic 5, 2 (June 1940), 56--68.Google ScholarCross Ref
- Coquand, T. and Huet, G.P. The calculus of constructions. Information and Computation 76, 2/3 (1988), 95--120. Google ScholarDigital Library
- Curien, P.-L., Herbelin, H. The duality of computation. In Proceedings of the International Conference on Functional Programming (Montreal, Canada, Sept. 18--20). ACM Press, New York, 2000, 233--243. Google ScholarDigital Library
- Curry, H.B. Functionality in combinatory logic. Proceedings of the National Academy of Science 20 (1934), 584--590.Google ScholarCross Ref
- Davies, R., Pfenning, F. A modal analysis of staged computation. In Principles of Programming Languages (St. Petersburg Beach, FL, 1996). 258--270. Google ScholarDigital Library
- de Bruijn, N.G. The mathematical language Automath, its usage, and some of its extensions. In Proceedings of the Symposium on Automatic Demonstration, Volume 125 of Lecture Notes in Computer Science (Versailles, France, Dec.). Springer-Verlag, 1968, 29--61.Google Scholar
- Gandy, R. The confluence of ideas in 1936. In The Universal Turing Machine: A Half-century Survey, R. Herken, Ed. Springer, 1995, 51--102. Google ScholarDigital Library
- Gentzen, G. Untersuchungen über das logische Schließen. Math. Z. 39, 2--3 (1935), 176--210, 405--431; reprinted in Szabo.<zref=R35>35<zrefx>Google Scholar
- Girard, J.Y. Interprétation functionelle et élimination des coupures dans l'arithm étique d'ordre supérieure. These D'Etat, Université Paris VII, 1972.Google Scholar
- Girard, J.-Y. Linear logic. Theoretical Computer Science 50 (1987), 1--102. Google ScholarDigital Library
- Gödel, K. Über formal unterscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Mathematik und Physik 38 (1931), 173--198; reprinted in Heijenoort.<zref=R37>37<zrefx>Google ScholarCross Ref
- Griffin, T. A formulae-as-types notion of control. In Proceedings of the 40th Annual Symposium on Principles of Programming Languages (Rome, Italy, Jan. 23--25). ACM Press, New York, 1990, 47--58. Google ScholarDigital Library
- Hindley, R. The principal type scheme of an object in combinatory logic. Transactions of the American Mathematical Society 146 (Dec. 1969), 29--60.Google Scholar
- Honda, K. Types for dyadic interaction. In Proceedings of the Fourth International Conference on Concurrency Theory (Hildesheim, Germany, Aug. 23--26, 1993), 509--523. Google ScholarDigital Library
- Howard, W.A. The formulae-as-types notion of construction. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism. Academic Press, 1980, 479--491; original version was circulated privately in 1969.Google Scholar
- Kleene, S. Origins of recursive function theory. Annals of the History of Computing 3, 1 (1981), 52--67. Google ScholarDigital Library
- Kleene, S.C. General recursive functions of natural numbers. Mathematical Annalen 112, 1 (Dec. 1936); abstract in Bulletin of the AMS (July 1935).Google ScholarCross Ref
- Lewis, C. and Langford, C. Symbolic Logic, 1938; reprinted by Dover, 1959.Google Scholar
- Martin-Löf, P. Intuitionistic Type Theory. Bibliopolis, Naples, Italy, 1984.Google Scholar
- Milner, R. A theory of type polymorphism in programming. Journal of Computer and System Sciences 17, 3 (1978), 348--375.Google ScholarCross Ref
- Mitchell, J.C., Plotkin, G.D. Abstract types have existential type. Transactions on Programming Languages and Systems 10, 3 (July 1988), 470--502. Google ScholarDigital Library
- Moggi, E. Notions of computation and monads. Information and Computation 93, 1 (1991), 55--92. Google ScholarDigital Library
- Murphy VII, T., Crary, K., Harper, R., Pfenning, F. A symmetric modal lambda calculus for distributed computing. In Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (Turku, Finland, July 13--17). IEEE Press, 2004, 286--295. Google ScholarDigital Library
- Murthy, C. An evaluation semantics for classical proofs. In Proceedings of Sixth Annual IEEE Symposium on Logic in Computer Science (Amsterdam, the Netherlands, July 15--18). IEEE Press, 1991, 96--107.Google ScholarCross Ref
- Parigot, M. λμ-calculus: An algorithmic interpretation of classical natural deduction. In Logic Programming and Automated Reasoning, Volume 624 of Lecture Notes in Computer Science. Springer-Verlag, 1992, 190--201. Google ScholarDigital Library
- Reynolds, J.C. Towards a theory of type structure. In Proceedings of the Symposium on Programming, Volume 19 of Lecture Notes in Computer Science (1974). 408--423. Google ScholarDigital Library
- Shell-Gellasch, A.E. Reflections of my advisor: Stories of mathematics and mathematicians. The Mathematical Intelligencer 25, 1 (2003), 35--41.Google ScholarCross Ref
- Szabo, M.E., Ed. The Collected Papers of Gerhard Gentzen. North Holland Publishing Co., Amsterdam, the Netherlands, 1969.Google Scholar
- Turing, A.M. On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society s2--42, 1 (1937); received May 28, 1936, read Nov. 12, 1936.Google ScholarCross Ref
- van Heijenoort, J. From Frege to Gödel: A Sourcebook in Mathematical Logic, 1879--1931. Harvard University Press, Cambridge, MA, 1967.Google Scholar
- Wadler, P. A taste of linear logic. In Proceedings of the 18th International Symposium on Mathematical Foundations of Computer Science Volume 711 of Lecture Notes on Computer Science (Gdańsk, Poland, Aug. 30--Sept. 3). Springer-Verlag, 1993, 185--210. Google ScholarDigital Library
- Wadler, P. Call-by-value is dual to call-by-name. In Proceedings of the International Conference on Functional Programming (Uppsala, Sweden, Aug. 25--29).ACM Press, New York, 2003, 189--201. Google ScholarDigital Library
- Wadler, P. Propositions as sessions. In Proceedings of the International Conference on Functional Programming (Copenhagen, Denmark, Sept. 10--12). ACM Press, New York, 2012, 273--286. Google ScholarDigital Library
Index Terms
- Propositions as types
Recommendations
Propositions as [Types]
Image factorizations in regular categories are stable under pullbacks, so they model a natural modal operator in dependent type theory. This unary type constructor [A] has turned up previously in a syntactic form as a way of erasing computational ...
Qualified types for MLF
Proceedings of the tenth ACM SIGPLAN international conference on Functional programmingMLF is a type system that extends a functional language with impredicative rank-n polymorphism. Type inference remains possible and only in some clearly defined situations, a local type annotation is required. Qualified types are a general concept that ...
Qualified types for MLF
ICFP '05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programmingMLF is a type system that extends a functional language with impredicative rank-n polymorphism. Type inference remains possible and only in some clearly defined situations, a local type annotation is required. Qualified types are a general concept that ...
Comments