Article

Languages of the future

Author:

Tim SheardAuthors Info & Claims

OOPSLA '04: Companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications

Pages 116 - 119

https://doi.org/10.1145/1028664.1028711

Published: 23 October 2004 Publication History

Abstract

This paper explores a new point in the design space of formal reasoning systems - part programming language, part logical framework. The system is built on a programming language where the user expresses equality constraints between types and the type checker then enforces these constraints. This simple extension to the type system allows the programmer to describe properties of his program in the types of witness objects which can be thought of as concrete evidence that the program has the property desired. These techniques and two other rich typing mechanisms, rank-N polymorphism and extensible kinds, create a powerful new programming idiom for writing programs whose types enforce semantic properties. This kind of synthesis between a practical programming language <i>and</i> a logic creates a foundation for the design of languages of the future.

References

[1]

P. Bertelsen. Semantics of Java Byte Code. Technical report, Dep. of Information Technology, Technical University of Denmark, March 1997.]]

[2]

Fréde'ric Besson, Thomas de Grenier de Latour, and Thomas Jensen. Secure calling contexts for stack inspection. In Proceedings of the Fourth ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP-02), pages 76--87, New York, October 6--8 2002. ACM Press.]]

Digital Library

[3]

Cristiano Calcagno, Eugenio Moggi, and Tim Sheard. Closed types for a safe imperative MetaML. Journal of Functional Programming, 13(12):545--572, May 2003.]]

Digital Library

[4]

Chiyan Chen and Hongwei Xi. Meta-programming through typeful code representation. In Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming (ICFP-03), ACM SIGPLAN Notices, pages 275--286, New York, August 25--29 2003. ACM Press.]]

Digital Library

[5]

James Cheney and Ralf Hinze. Phantom types. Available from http://www.informatik.uni-bonn.de ralf/publications/Phantom.pdf|.,2003.]]

[6]

Karl Crary and Stephanie Weirich. Resource bound certification. In Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POLP-00), pages 184--198, N.Y., January 19--21 2000. ACM Press.]]

Digital Library

[7]

Simon Peyton Jones and Mark Shields. Practical type inference for arbitrary-rank types. Technical report, Microsoft Research, "December" 2003. http://research.microsoft.com/Users/simonpj/papers/putting/index.htm.]]

[8]

J. Launchbury and R. Paterson. Parametricity and unboxing with unpointed types. Lecture Notes in Computer Science, 1058:204--??, 1996.]]

Digital Library

[9]

Didier Le Botlan and Didier Rémy. MLF: raising ML to the power of system F. ACM SIGPLAN Notices, 38(9):27--38, September 2003.]]

Digital Library

[10]

G. Morrisett, D. Walker, K. Crary, and N. Glew. From system F to typed assembly language. ACM Transactions on Programming Languages and Systems (TOPLAS), 21(3):528--569, May 1999.]]

Digital Library

[11]

Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. TALx86: A realistic typed assembly language. ACM SIGPLAN Workshop on Compiler Support for System Software, 1999.]]

[12]

P. Ørbæk and J. Palsberg. Trust in the λ-calculus. Journal of Functional Programming, 7(6):557--591, November 1997.]]

Digital Library

[13]

Lawrence C. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and Computer Science, pages 361--386. Academic Press, 1990.]]

[14]

Frank Pfenning and Carsten Schürmann. System description: Twelf---A meta-logical framework for deductive systems. In Harald Ganzinger, editor, Proceedings of the 16th International Conference on Automated Deduction (CADE-16), volume 1632 of LNAI, pages 202--206, Berlin, July 7--10, 1999. Springer-Verlag.]]

Digital Library

[15]

Andrei Sabelfeld and Andrew C. Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21(1):5--19, January 2003.]]

Digital Library

[16]

T. Sheard and S. Peyton-Jones. Template meta-programming for haskell. In Proceedings of the ACM SIGPLAN Haskell Workshop, pages 1--16. ACM, 2002.]]

Digital Library

[17]

Vincent Simonet. An extension of HM(X) with bounded existential and universal data-types. ACM SIGPLAN Notices, 38(9):39--50, September 2003.]]

Digital Library

[18]

R. Stata and M. Abadi. A type system for Java bytecode subroutines. In 25th Annual ACM Symposium on Principles of Programming Languages, pages 149--160, January 1998.]]

Digital Library

[19]

Walid Taha. A sound reduction semantics for untyped CBN mutli-stage computation. Or, the theory of MetaML is non-trivial. In 2000 SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'00), January 2000.]]

Digital Library

[20]

Walid Taha and Tim Sheard. MetaML: Multi-stage programming with explicit annotations. Theoretical Computer Science, 248(1-2), 2000.]]

Digital Library

[21]

The Coq Development Team. The Coq Proof Assistant Reference Manual, Version 7.4. INRIA, 2003. http://pauillac.inria.fr/coq/doc/main.html.]]

[22]

Joseph C. Vanderwaart and Karl Crary. Foundational typed assembly language for grid computing. Technical Report CMU-CS-04-104, Carnegie Mellon University, 2004.]]

[23]

Dennis Volpano, Geoffrey Smith, and Cynthia Irvine. A sound type system for secure flow analysis. Journal of Computer Security, 4(3):167--187, December 1996.]]

Digital Library

[24]

Philip Wadler. Comprehending monads. Proceedings of the ACM Symposium on Lisp and Functional Programming, Nice, France, pages 61--78, June 1990.]]

Digital Library

[25]

Philip Wadler. The essence of functional programming (invited talk). In 19'th ACM Symposium on Principles of Programming Languages, Albuquerque, New Mexico, January 1992.]]

Digital Library

[26]

Philip Wadler. Monads for functional programming. In M. Broy, editor, Program Design Calculi, volume 118 of NATO ASI series, Series F: Computer and System Sciences. Springer Verlag, 1994. Proceedings of the International Summer School at Marktoberdorf directed by F. L. Bauer, M. Broy, E. W. Dijkstra, D. Gries, and C. A. R. Hoare.]]

[27]

D. S. Wallach and E. W. Felten. Understanding java stack inspection. In 1998 IEEE Symposium on Security and Privacy (SSP '98), pages 52--65, Washington - Brussels - Tokyo, May 1998. IEEE.]]

[28]

Hongwei Xi and Frank Pfenning. Eliminating array bound checking through dependent types. ACM SIGPLAN Notices, 33(5):249--257, May 1998.]]

Digital Library

[29]

Hongwei Xi and Frank Pfenning. Dependent types in practical programming. In ACM, editor, POPL '99. Proceedings of the 26th ACM SIGPLAN-SIGACT on Principles of programming languages, January 20--22, 1999, San Antonio, TX, ACM SIGPLAN Notices, pages 214--227, New York, NY, USA, 1999. ACM Press.]]

Digital Library

Cited By

Martínez AScholliers CSinger J(2022)A Language Based on Two Relations between SymbolsProceedings of the 2022 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software10.1145/3563835.3567660(95-111)Online publication date: 29-Nov-2022
https://dl.acm.org/doi/10.1145/3563835.3567660
Karachalias GSchrijvers TVytiniotis DJones S(2015)GADTs meet their match: pattern-matching warnings that account for GADTs, guards, and lazinessACM SIGPLAN Notices10.1145/2858949.278474850:9(424-436)Online publication date: 29-Aug-2015
https://dl.acm.org/doi/10.1145/2858949.2784748
Karachalias GSchrijvers TVytiniotis DJones SFisher KReppy J(2015)GADTs meet their match: pattern-matching warnings that account for GADTs, guards, and lazinessProceedings of the 20th ACM SIGPLAN International Conference on Functional Programming10.1145/2784731.2784748(424-436)Online publication date: 29-Aug-2015
https://dl.acm.org/doi/10.1145/2784731.2784748
Show More Cited By

Index Terms

Languages of the future
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages

Recommendations

Languages of the future

This paper explores a new point in the design space of formal reasoning systems - part programming language, part logical framework. The system is built on a programming language where the user expresses equality constraints between types and the type ...
Supporting compile-time debugging and precise error reporting in meta-programs
TOOLS'12: Proceedings of the 50th international conference on Objects, Models, Components, Patterns

Compile-time meta-programming is an advanced language feature enabling to mix programs with definitions that are executed at compile-time and may generate source code to be put in their place. Such definitions are called meta-programs and their actual ...
Languages as libraries
PLDI '11

Programming language design benefits from constructs for extending the syntax and semantics of a host language. While C's string-based macros empower programmers to introduce notational shorthands, the parser-level macros of Lisp encourage ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

OOPSLA '04: Companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications

October 2004

348 pages

ISBN:1581138334

DOI:10.1145/1028664

Conference Chair:
John Vlissides
IBM Research
,
Program Chairs:
Doug Schmidt
Vanderbilt University
,
Geoff Cohen
Coherence Engine

Copyright © 2004 ACM.

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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 October 2004

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

OOPSLA04

Sponsor:

OOPSLA04: ACM SIGPLAN Object Oriented Programming Systems and Applications Conference

October 24 - 28, 2004

BC, Vancouver, CANADA

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

57
Total Citations
View Citations
490
Total Downloads

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

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Martínez AScholliers CSinger J(2022)A Language Based on Two Relations between SymbolsProceedings of the 2022 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software10.1145/3563835.3567660(95-111)Online publication date: 29-Nov-2022
https://dl.acm.org/doi/10.1145/3563835.3567660
Karachalias GSchrijvers TVytiniotis DJones S(2015)GADTs meet their match: pattern-matching warnings that account for GADTs, guards, and lazinessACM SIGPLAN Notices10.1145/2858949.278474850:9(424-436)Online publication date: 29-Aug-2015
https://dl.acm.org/doi/10.1145/2858949.2784748
Karachalias GSchrijvers TVytiniotis DJones SFisher KReppy J(2015)GADTs meet their match: pattern-matching warnings that account for GADTs, guards, and lazinessProceedings of the 20th ACM SIGPLAN International Conference on Functional Programming10.1145/2784731.2784748(424-436)Online publication date: 29-Aug-2015
https://dl.acm.org/doi/10.1145/2784731.2784748
Day LHutton GPlasmeijer R(2013)Compilation à la CarteProceedings of the 25th symposium on Implementation and Application of Functional Languages10.1145/2620678.2620680(13-24)Online publication date: 28-Aug-2013
https://dl.acm.org/doi/10.1145/2620678.2620680
Benton NHur CKennedy AMcbride C(2012)Strongly Typed Term Representations in CoqJournal of Automated Reasoning10.1007/s10817-011-9219-049:2(141-159)Online publication date: 1-Aug-2012
https://dl.acm.org/doi/10.1007/s10817-011-9219-0
Iordanov B(2010)HyperGraphDBProceedings of the 2010 international conference on Web-age information management10.5555/1927585.1927589(25-36)Online publication date: 15-Jul-2010
https://dl.acm.org/doi/10.5555/1927585.1927589
Brady EHammond K(2010)Correct-by-Construction Concurrency: Using Dependent Types to Verify Implementations of Effectful Resource Usage ProtocolsFundamenta Informaticae10.5555/1883634.1883636102:2(145-176)Online publication date: 1-Apr-2010
https://dl.acm.org/doi/10.5555/1883634.1883636
Chlipala A(2010)UrACM SIGPLAN Notices10.1145/1809028.180661245:6(122-133)Online publication date: 5-Jun-2010
https://dl.acm.org/doi/10.1145/1809028.1806612
Chlipala AZorn BAiken A(2010)UrProceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/1806596.1806612(122-133)Online publication date: 5-Jun-2010
https://dl.acm.org/doi/10.1145/1806596.1806612
Iordanov B(2010)HyperGraphDB: A Generalized Graph DatabaseWeb-Age Information Management10.1007/978-3-642-16720-1_3(25-36)Online publication date: 2010
https://doi.org/10.1007/978-3-642-16720-1_3
Show More Cited By

View Options

Login options

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

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents