Article

Free access

Theorems for free!

Author:

FPCA '89: Proceedings of the fourth international conference on Functional programming languages and computer architecture

Pages 347 - 359

https://doi.org/10.1145/99370.99404

Published: 01 November 1989 Publication History

PDF eReader

References

[1]

V. Breazu-Tannen, T. Coquand, C. A. Gunter, and A. Scedrov, Inheritance and explicit coercion. In $'th Angual Symposium on Logic ir~ Computer Science, Asilomar, California, June 1989.

Digital Library

Google Scholar

[2]

E. S. Bainbridge, P. J. Freyd, A. Scedrov, and P. J. Scott, Functorial polymorphism. In G. Huet, editor, Logical Foundations of Functional Programming, Austin, Texas, 1987. Addison-Wesley, to appear.

Google Scholar

[3]

K.B. Bruce and A. R. Meyer, The semantics of second-order polymorphic lambda cal. culus. In Kahn, MacQueen, and Plotkin, editors, $emaatics of Data Types, Sophia- Antipolis, France, 1984, pp. 131-144. LNCS 173, Springer-Verlag.

Digital Library

Google Scholar

[4]

V. Breazu-Tannen and T. Coquand, Extensional models for polymorphism. Theoretical Computer Science, 59:85-114, 1988.

Digital Library

Google Scholar

[5]

G. Barrett and P. Wadler, Derivation of a pattern-matching compiler. Manuscript, Programming Research Group, Oxford, 1986.

Google Scholar

[6]

R. Bird and P. Wadler, Introduction to Functional Programming. Prentice Hall, 1988.

Digital Library

Google Scholar

[7]

L. Damns and R. MiMer, Principal type schemes for functional programs. In Proceedings of the 9'th Annual Symposium og Principles o/Programming Languages, Albuquerque, N.M., January 1982.

Digital Library

Google Scholar

[8]

P.J. deBruin, Naturalness of polymorphism. Submitted to Category Theory and Computer Science, Manchester, 1989.

Google Scholar

[9]

P. J. Freyd, J. Y. Girard, A. Scedrov, and P. J. Scott, Semantic parametricity in polymorphic lambda calculus. In $'rd A~nual Symposium on Logic in Computer Science, Edinburgh, Scotland, June 1988.

Google Scholar

[10]

S. Fortune, D. Leivant, and M. O'Donnell, The expressiveness of simple and secondorder type structures. Journal of the A CM, 30(1):151-185, January 1983.

Digital Library

Google Scholar

[11]

J.-Y. Girard, Interpretation fu~ctior~elle et $limination des coupures dens l~arithm~tique d'ordre sup~rieure. Ph.D. thesis, Universit~ Paris VII, 1972.

Google Scholar

[12]

J.-Y. Girard, The system F of variable types, fifteen years later. Theoretical Computer Science, 45, pp. 159-192.

Digital Library

Google Scholar

[13]

J.-Y. Girard, Y. Lefont, and P. Taylor, Proofs agd Types. Cambridge University Press, 1989.

Digital Library

Google Scholar

[14]

R. Hindley, The principal type scheme of an object in combinatory logic. Trans. Am. M~tk. Soc. i~6, pp. 29-60, December 1969.

Google Scholar

[15]

P. Hudak and P. Wadler, editors, Report on the Functional Programming Language HazkeIL Technical Report YALEU/DCS/ RR656, Yale University, Department of Computer Science, December 1988; also Technical Report, Glasgow University, Department of Computer Science, December 1988.

Google Scholar

[16]

J. Meseguer, Relating models of polymorphism. In 16'th A CM Symposium o~ Principle8 of Programming Languages, Austin, Texas, January 1989.

Digital Library

Google Scholar

[17]

R. Milner, A theory of type polymorphism in programming. J. ~orapgt. $yst. $ci. 17, pp. 348-375, 1978.

Google Scholar

[18]

R. Milner, A proposal for Standard ML. In A CM Symposium on Lisp and Functional Programming, Austin, Texas, August 1984.

Digital Library

Google Scholar

[19]

R. Milner, Changes to the Standard ML core language. Report ECS-LFCS-87-33, Edinburgh University, Computer Science Dept., 1987.

Google Scholar

[20]

3. C. Mitchell, Representation independence and data abstraction. In 13'th A CM Symposium on Principles of Programming La~- ~uages, pp. 263-276.

Digital Library

Google Scholar

[21]

J.C. Mitchell and A. R. Meyer, Second-order logical relations. In R. Parikh, editor, Logics of Programs, Brooklyn, New York, 1985. LNCS 193, Springer-Verlag.

Digital Library

Google Scholar

[22]

A.M. Pitts, Polymorphism is set theoretic, constructively. In D. H. Pitt, et al., editors, Category Theory and Computer Science, Edinburgh, 1987. LNCS 283, Springer-Verlag.

Digital Library

Google Scholar

[23]

J.C. Reynolds, Towards a theory of type structure. In B. Robinet, editor, Proc. Colloque rut la Programmatio~, LNCS 19, S pringer-Verlag.

Digital Library

Google Scholar

[24]

J.C. Reynolds, Types, abstraction, and parametric polymorphism, in R. E. A. Mason, editor, Information Processing 83, pp. 513-523. North-Holland, Amsterdam.

Google Scholar

[25]

J.C. Reynolds, Polymorphism is not set theoretic. In Kahn, MacQueen, and Plotkin, editors, Semantics of Data Types, Sophia- Antipolis, France, 1984, pp. 145-156. LNCS 173, Springer-Verlag.

Google Scholar

[26]

J.C. Reynolds, Three approaches to type structure. In Mathematical Fou~datio~ of Software Development, LNCS 185, Springer- Verlag, 1985.

Digital Library

Google Scholar

[27]

M. Sheeran, Categories for the working hardware designer. In Workshop on Hardware Specification, Verification, and Synthesis: Mathematical Aspects, Cornell, July 1989.

Digital Library

Google Scholar

[28]

D.A. Turner, Miranda: A non-strict functional language with polymorphic types. In Proceedings of the ~%d international Conference on Functional Programmir~g Languages a~d Computer Architecture, Nancy, France, September 1985. LNCS 201, Springer-Verlag, 1985.

Digital Library

Google Scholar

[29]

P. Wadler and S. Blott, How to make adho~ polymorphism less ad ho~. In 16'th A CM Symposium on Principles of Programming Languages, Austin, Texas, January 1989.

Digital Library

Google Scholar

Cited By

View all

Traversié T(2024)Proofs for Free in the λΠ-Calculus Modulo TheoryElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.404.4404(49-63)Online publication date: 8-Jul-2024
https://doi.org/10.4204/EPTCS.404.4
Ma CGe ZLee EZhang Y(2024)Lexical Effect Handlers, DirectlyProceedings of the ACM on Programming Languages10.1145/36897708:OOPSLA2(1670-1698)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689770
Lobo-Vesga ERusso AGaboardi MCortiñas C(2024)Sensitivity by ParametricityProceedings of the ACM on Programming Languages10.1145/36897268:OOPSLA2(415-441)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689726
Show More Cited By

Index Terms

Theorems for free!

Recommendations

New inequalities from classical Sturm theorems

Inequalities satisfied by the zeros of the solutions of second-order hypergeometric equations are derived through a systematic use of Liouville transformations together with the application of classical Sturm theorems. This systematic study allows us to ...
Interlacing theorems for the zeros of some orthogonal polynomials from different sequences

We study the interlacing properties of the zeros of orthogonal polynomials p"n and r"m, m=n or n-1 where {p"n}"n"="1^~ and {r"m}"m"="1^~ are different sequences of orthogonal polynomials. The results obtained extend a conjecture by Askey, that the zeros ...
Applications of q-Taylor theorems

We establish two new q-analogues of a Taylor series expansion for polynomials using special Askey-Wilson polynomial bases. Combining these expansions with an earlier expansion theorem we derive inverse relations and evaluate certain linearization ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

FPCA '89: Proceedings of the fourth international conference on Functional programming languages and computer architecture

November 1989

395 pages

ISBN:0897913280

DOI:10.1145/99370

Chairman:
Joseph E. Stoy

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 ACM 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: 01 November 1989

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

FPCA89

Sponsor:

SIGPLAN
IFIP WG 2.8
SIGARCH

FPCA89: The International Conference on Functional Programming Languages & Computer Architectures

September 11 - 13, 1989

Imperial College, London, United Kingdom

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

478
Total Citations
View Citations
10,047
Total Downloads

Downloads (Last 12 months)3,302
Downloads (Last 6 weeks)425

Reflects downloads up to 22 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Traversié T(2024)Proofs for Free in the λΠ-Calculus Modulo TheoryElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.404.4404(49-63)Online publication date: 8-Jul-2024
https://doi.org/10.4204/EPTCS.404.4
Ma CGe ZLee EZhang Y(2024)Lexical Effect Handlers, DirectlyProceedings of the ACM on Programming Languages10.1145/36897708:OOPSLA2(1670-1698)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689770
Lobo-Vesga ERusso AGaboardi MCortiñas C(2024)Sensitivity by ParametricityProceedings of the ACM on Programming Languages10.1145/36897268:OOPSLA2(415-441)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689726
Mulleners NJeuring JHeeren B(2024)Example-Based Reasoning about the Realizability of Polymorphic ProgramsProceedings of the ACM on Programming Languages10.1145/36746368:ICFP(317-337)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674636
Blanchi VPaquet HSobocinski PLago UEsparza J(2024)Element-free probability distributions and random partitionsProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662131(1-14)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662131
Chen TSiek J(2024)Quest Complete: The Holy Grail of Gradual SecurityProceedings of the ACM on Programming Languages10.1145/36564428:PLDI(1609-1632)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656442
Igarashi AOzaki SSekiyama TTanabe Y(2024)Space-Efficient Polymorphic Gradual Typing, Mostly ParametricProceedings of the ACM on Programming Languages10.1145/36564418:PLDI(1585-1608)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656441
DeYoung HMordido APfenning FDas A(2024)Parametric Subtyping for Structural Parametric PolymorphismProceedings of the ACM on Programming Languages10.1145/36329328:POPL(2700-2730)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632932
Borkowski MVazou NJhala R(2024)Mechanizing Refinement TypesProceedings of the ACM on Programming Languages10.1145/36329128:POPL(2099-2128)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632912
Sieczkowski FStepanenko SSterling JBirkedal L(2024)The Essence of Generalized Algebraic Data TypesProceedings of the ACM on Programming Languages10.1145/36328668:POPL(695-723)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632866
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

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

Cited By

Index Terms

Recommendations

New inequalities from classical Sturm theorems

Interlacing theorems for the zeros of some orthogonal polynomials from different sequences

Applications of q-Taylor theorems