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.

Digital Library

Google Scholar

[5]

Carroll, L. What the Tortoise said to Achilles. Mind 4, 14 (Apr. 1895), 278--280.

Google Scholar

[6]

Church, A. A set of postulates for the foundation of logic. Ann. Math. 33, 2 (1932), 346--366.

Crossref

Google Scholar

[7]

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).

Crossref

Google Scholar

[8]

Church, A. A formulation of the simple theory of types. Journal of Symbolic Logic 5, 2 (June 1940), 56--68.

Crossref

Google Scholar

[9]

Coquand, T. and Huet, G.P. The calculus of constructions. Information and Computation 76, 2/3 (1988), 95--120.

Digital Library

Google Scholar

[10]

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.

Digital Library

Google Scholar

[11]

Curry, H.B. Functionality in combinatory logic. Proceedings of the National Academy of Science 20 (1934), 584--590.

Crossref

Google Scholar

[12]

Davies, R., Pfenning, F. A modal analysis of staged computation. In Principles of Programming Languages (St. Petersburg Beach, FL, 1996). 258--270.

Digital Library

Google Scholar

[13]

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

[14]

Gandy, R. The confluence of ideas in 1936. In The Universal Turing Machine: A Half-century Survey, R. Herken, Ed. Springer, 1995, 51--102.

Digital Library

Google Scholar

[15]

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

[16]

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

[17]

Girard, J.-Y. Linear logic. Theoretical Computer Science 50 (1987), 1--102.

Digital Library

Google Scholar

[18]

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>}

Crossref

Google Scholar

[19]

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.

Digital Library

Google Scholar

[20]

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

[21]

Honda, K. Types for dyadic interaction. In Proceedings of the Fourth International Conference on Concurrency Theory (Hildesheim, Germany, Aug. 23--26, 1993), 509--523.

Digital Library

Google Scholar

[22]

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

[23]

Kleene, S. Origins of recursive function theory. Annals of the History of Computing 3, 1 (1981), 52--67.

Digital Library

Google Scholar

[24]

Kleene, S.C. General recursive functions of natural numbers. Mathematical Annalen 112, 1 (Dec. 1936); abstract in Bulletin of the AMS (July 1935).

Crossref

Google Scholar

[25]

Lewis, C. and Langford, C. Symbolic Logic, 1938; reprinted by Dover, 1959.

Google Scholar

[26]

Martin-Löf, P. Intuitionistic Type Theory. Bibliopolis, Naples, Italy, 1984.

Google Scholar

[27]

Milner, R. A theory of type polymorphism in programming. Journal of Computer and System Sciences 17, 3 (1978), 348--375.

Crossref

Google Scholar

[28]

Mitchell, J.C., Plotkin, G.D. Abstract types have existential type. Transactions on Programming Languages and Systems 10, 3 (July 1988), 470--502.

Digital Library

Google Scholar

[29]

Moggi, E. Notions of computation and monads. Information and Computation 93, 1 (1991), 55--92.

Digital Library

Google Scholar

[30]

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.

Digital Library

Google Scholar

[31]

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.

Crossref

Google Scholar

[32]

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.

Digital Library

Google Scholar

[33]

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.

Digital Library

Google Scholar

[34]

Shell-Gellasch, A.E. Reflections of my advisor: Stories of mathematics and mathematicians. The Mathematical Intelligencer 25, 1 (2003), 35--41.

Crossref

Google Scholar

[35]

Szabo, M.E., Ed. The Collected Papers of Gerhard Gentzen. North Holland Publishing Co., Amsterdam, the Netherlands, 1969.

Google Scholar

[36]

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.

Crossref

Google Scholar

[37]

van Heijenoort, J. From Frege to Gödel: A Sourcebook in Mathematical Logic, 1879--1931. Harvard University Press, Cambridge, MA, 1967.

Google Scholar

[38]

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.

Digital Library

Google Scholar

[39]

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.

Digital Library

Google Scholar

[40]

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.

Digital Library

Google Scholar

Cited By

View all

OLIVEIRA J(2025)How much is in a square? Calculating functional programs with squaresJournal of Functional Programming10.1017/S095679682500001235Online publication date: 26-Feb-2025
https://doi.org/10.1017/S0956796825000012
Annus TJoram PAlves SCockx J(2024)Term Search in RustProceedings of the 9th ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3678000.3678210(62-73)Online publication date: 28-Aug-2024
https://dl.acm.org/doi/10.1145/3678000.3678210
Dorn CPribadi H(2024)TypeQL: A Type-Theoretic & Polymorphic Query LanguageProceedings of the ACM on Management of Data10.1145/36516112:2(1-27)Online publication date: 14-May-2024
https://dl.acm.org/doi/10.1145/3651611
Show More Cited By

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 programming

MLF 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 programming

MLF 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

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

Communications of the ACM Volume 58, Issue 12

December 2015

115 pages

ISSN:0001-0782

EISSN:1557-7317

DOI:10.1145/2847579

Editor:
Moshe Y. Vardi
Association for Computing Machinery, New York, NY

Issue’s Table of Contents

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 November 2015

Published in CACM Volume 58, Issue 12

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article
Popular
Refereed

Funding Sources

Engineering and Physical Sciences Research Council

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

92
Total Citations
View Citations
16,936
Total Downloads

Downloads (Last 12 months)2,016
Downloads (Last 6 weeks)204

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

OLIVEIRA J(2025)How much is in a square? Calculating functional programs with squaresJournal of Functional Programming10.1017/S095679682500001235Online publication date: 26-Feb-2025
https://doi.org/10.1017/S0956796825000012
Annus TJoram PAlves SCockx J(2024)Term Search in RustProceedings of the 9th ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3678000.3678210(62-73)Online publication date: 28-Aug-2024
https://dl.acm.org/doi/10.1145/3678000.3678210
Dorn CPribadi H(2024)TypeQL: A Type-Theoretic & Polymorphic Query LanguageProceedings of the ACM on Management of Data10.1145/36516112:2(1-27)Online publication date: 14-May-2024
https://dl.acm.org/doi/10.1145/3651611
Watkins EChen J(2024)The four-fifths rule is not disparate impact: A woeful tale of epistemic trespassing in algorithmic fairnessProceedings of the 2024 ACM Conference on Fairness, Accountability, and Transparency10.1145/3630106.3658938(764-775)Online publication date: 3-Jun-2024
https://dl.acm.org/doi/10.1145/3630106.3658938
Kang AGalhotra S(2024)TQL: Towards Type-Driven Data Discovery2024 IEEE International Conference on Big Data (BigData)10.1109/BigData62323.2024.10825227(7338-7343)Online publication date: 15-Dec-2024
https://doi.org/10.1109/BigData62323.2024.10825227
Bengio YMalkin N(2024)Machine Learning and Information Theory Concepts towards an AI MathematicianBulletin of the American Mathematical Society10.1090/bull/183961:3(457-469)Online publication date: 15-May-2024
https://doi.org/10.1090/bull/1839
Smola FFleuriot J(2024)Linear Resources in Isabelle/HOLJournal of Automated Reasoning10.1007/s10817-024-09698-268:2Online publication date: 18-May-2024
https://dl.acm.org/doi/10.1007/s10817-024-09698-2
Myers DSati HSchreiber U(2024)Topological Quantum Gates in Homotopy Type TheoryCommunications in Mathematical Physics10.1007/s00220-024-05020-8405:7Online publication date: 8-Jul-2024
https://doi.org/10.1007/s00220-024-05020-8
Vasilenko EVazou NBarthe G(2024)OBRA: Oracle-Based, Relational, Algorithmic Type VerificationProgramming Languages and Systems10.1007/978-981-97-8943-6_14(283-302)Online publication date: 23-Oct-2024
https://dl.acm.org/doi/10.1007/978-981-97-8943-6_14
Caires LToninho B(2024)The Session Abstract MachineProgramming Languages and Systems10.1007/978-3-031-57262-3_9(206-235)Online publication date: 5-Apr-2024
https://doi.org/10.1007/978-3-031-57262-3_9
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Digital Edition

View this article in digital edition.

Digital Edition

Magazine Site

View this article on the magazine site (external)

Magazine Site

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract

Supplementary Material

References

Cited By

Index Terms

Recommendations

Propositions as [Types]

Qualified types for MLF

Qualified types for MLF

Comments

Information

Published In

Publisher

Publication History

Permissions

Check for updates

Qualifiers

Funding Sources

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Digital Edition

Magazine Site

Login options

Full Access

Share

Share this Publication link

Share on social media

Affiliations