Article

The semantics of second order polymorphic lambda calculus.

Authors:

Kim B. Bruce,

Albert R. MeyerAuthors Info & Claims

Proc. of the international symposium on Semantics of data types

Pages 131 - 156

Published: 01 July 1984 Publication History

Abstract

No abstract available.

Cited By

View all

Abel A(2009)Typed applicative structures and normalization by evaluation for system FωProceedings of the 23rd CSL international conference and 18th EACSL Annual conference on Computer science logic10.5555/1807662.1807671(40-54)Online publication date: 7-Sep-2009
https://dl.acm.org/doi/10.5555/1807662.1807671
Johann P(2005)On proving the correctness of program transformations based on free theorems for higher-order polymorphic calculiMathematical Structures in Computer Science10.1017/S096012950400457815:2(201-229)Online publication date: 1-Apr-2005
https://dl.acm.org/doi/10.1017/S0960129504004578
Wadler PStoy J(1989)Theorems for free!Proceedings of the fourth international conference on Functional programming languages and computer architecture10.1145/99370.99404(347-359)Online publication date: 1-Nov-1989
https://dl.acm.org/doi/10.1145/99370.99404
Show More Cited By

Index Terms

The semantics of second order polymorphic lambda calculus.

Recommendations

Pedagogical second-order λ-calculus

The present work introduces the notion of pedagogical natural deduction systems, i.e. natural deduction systems for which hypotheses occurring in a proof must be motivated by an example. In formal terms, we replace the rule (Hyp): by the rule (P-Hyp): ...
Programming Language Semantics Using Extensional $\lambda$-Calculus Models
A cut-free calculus for second-order Gödel logic

We prove that the extension of the known hypersequent calculus for standard first-order Gödel logic with usual rules for second-order quantifiers is sound and (cut-free) complete for Henkin-style semantics for second-order Gödel logic. The proof is ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

Proc. of the international symposium on Semantics of data types

July 1984

391 pages

ISBN:3540133461

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 July 1984

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 09 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Abel A(2009)Typed applicative structures and normalization by evaluation for system FωProceedings of the 23rd CSL international conference and 18th EACSL Annual conference on Computer science logic10.5555/1807662.1807671(40-54)Online publication date: 7-Sep-2009
https://dl.acm.org/doi/10.5555/1807662.1807671
Johann P(2005)On proving the correctness of program transformations based on free theorems for higher-order polymorphic calculiMathematical Structures in Computer Science10.1017/S096012950400457815:2(201-229)Online publication date: 1-Apr-2005
https://dl.acm.org/doi/10.1017/S0960129504004578
Wadler PStoy J(1989)Theorems for free!Proceedings of the fourth international conference on Functional programming languages and computer architecture10.1145/99370.99404(347-359)Online publication date: 1-Nov-1989
https://dl.acm.org/doi/10.1145/99370.99404
Meseguer J(1989)Relating models of polymorphismProceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/75277.75297(228-241)Online publication date: 3-Jan-1989
https://dl.acm.org/doi/10.1145/75277.75297
Martini SChailloux J(1988)Bounded quantifiers have interval modelsProceedings of the 1988 ACM conference on LISP and functional programming10.1145/62678.62699(164-173)Online publication date: 1-Jan-1988
https://dl.acm.org/doi/10.1145/62678.62699
Meyer AReinhold M(1986)"Type" is not a typeProceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages10.1145/512644.512671(287-295)Online publication date: 1-Jan-1986
https://dl.acm.org/doi/10.1145/512644.512671
Mitchell J(1986)Representation independence and data abstractionProceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages10.1145/512644.512669(263-276)Online publication date: 1-Jan-1986
https://dl.acm.org/doi/10.1145/512644.512669
Bruce KWegner PWegner PShriver B(1986)An algebraic model of sybtypes in object-oriented languages (draft)Proceedings of the 1986 SIGPLAN workshop on Object-oriented programming10.1145/323779.323756(163-172)Online publication date: 1-Jun-1986
https://dl.acm.org/doi/10.1145/323779.323756
Bruce KWegner P(1986)An algebraic model of sybtypes in object-oriented languages (draft)ACM SIGPLAN Notices10.1145/323648.32375621:10(163-172)Online publication date: 1-Jun-1986
https://dl.acm.org/doi/10.1145/323648.323756
Mitchell JScherlis WWilliams JGabriel R(1986)A type-inference approach to reduction properties and semantics of polymorphic expressions (summary)Proceedings of the 1986 ACM conference on LISP and functional programming10.1145/319838.319872(308-319)Online publication date: 8-Aug-1986
https://dl.acm.org/doi/10.1145/319838.319872
Show More Cited By

View Options

View options

Login options

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

Abstract

Cited By

Index Terms

Recommendations

Pedagogical second-order λ-calculus

Programming Language Semantics Using Extensional $\lambda$-Calculus Models

A cut-free calculus for second-order Gödel logic

Comments

Information

Published In

Publisher

Publication History

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations