*banner
 

A Formalization of the Ptolemy II Type System
Chris Shaver, Marten Lohstroh

Citation
Chris Shaver, Marten Lohstroh. "A Formalization of the Ptolemy II Type System". Talk or presentation, 7, November, 2013; Presented at the 10th Biennial Ptolemy Miniconference.

Abstract
Type systems have been studied extensively, particularly in the context of functional programming, and a great number of provable mathematical results have been determined for a wide range of such systems. Type checking imposes a simple and often decidable form of verification on programs in typed languages, and can eliminate large classes of erroneously constructed programs during the development process of complex software systems. The Ptolemy II modeling platform has a sophisticated type system used for both static and dynamic type checking. Where types are not explicitly given in models, Ptolemy II can also infer them from context. To study the type system rigorously, and relate it to existing results on formal type systems to understand its properties, this type system needs to first be put into the formal language used in the study of type systems. Specifically, a type syntax must be given to describe the set of possible types that can be inductively constructed out of primitive ones. A static semantics must also be given in the form of a set of type judgments constituting well­-typed models: ones deemed correct under the type system. To define this set, an inductive collection of derivations must be given. Only with these elements clearly defined can the type system of Ptolemy II be compared to those extensively studied in type theory. In this presentation we introduce the Ptolemy II type system by informally describing its capabilities and discussing a number of practical use cases that illustrate its limitations. Subsequently, we present a corresponding formal specification in terms of a formal syntax for Ptolemy II models and a set of type judgements, which then we relate to a type system known as HM(X): Hindley-Milner over a constraint system. Finally, we discuss potential changes to Ptolemy II type system that may be worth further investigation.

Electronic downloads

  • PtypeSys.pdf · application/pdf · 909 kbytes. (PDF version of the slides presented at the Tenth Biennial Ptolemy Miniconference.)
Citation formats  
  • HTML
    Chris Shaver, Marten Lohstroh. <a
    href="http://chess.eecs.berkeley.edu/pubs/1036.html"><i>A
    Formalization of the Ptolemy II Type
    System</i></a>, Talk or presentation,  7,
    November, 2013; Presented at the <a
    href="http://ptolemy.eecs.berkeley.edu/conferences/13/"
    >10th Biennial Ptolemy Miniconference</a>.
  • Plain text
    Chris Shaver, Marten Lohstroh. "A Formalization of the
    Ptolemy II Type System". Talk or presentation,  7,
    November, 2013; Presented at the <a
    href="http://ptolemy.eecs.berkeley.edu/conferences/13/"
    >10th Biennial Ptolemy Miniconference</a>.
  • BibTeX
    @presentation{ShaverLohstroh13_FormalizationOfPtolemyIITypeSystem,
        author = {Chris Shaver and Marten Lohstroh},
        title = {A Formalization of the Ptolemy II Type System},
        day = {7},
        month = {November},
        year = {2013},
        note = {Presented at the <a
                  href="http://ptolemy.eecs.berkeley.edu/conferences/13/"
                  >10th Biennial Ptolemy Miniconference</a>.},
        abstract = {Type systems have been studied extensively,
                  particularly in the context of functional
                  programming, and a great number of provable
                  mathematical results have been determined for a
                  wide range of such systems. Type checking imposes
                  a simple and often decidable form of verification
                  on programs in typed languages, and can eliminate
                  large classes of erroneously constructed programs
                  during the development process of complex software
                  systems. The Ptolemy II modeling platform has a
                  sophisticated type system used for both static and
                  dynamic type checking. Where types are not
                  explicitly given in models, Ptolemy II can also
                  infer them from context. To study the type system
                  rigorously, and relate it to existing results on
                  formal type systems to understand its properties,
                  this type system needs to first be put into the
                  formal language used in the study of type systems.
                  Specifically, a type syntax must be given to
                  describe the set of possible types that can be
                  inductively constructed out of primitive ones. A
                  static semantics must also be given in the form of
                  a set of type judgments constituting well­-typed
                  models: ones deemed correct under the type system.
                  To define this set, an inductive collection of
                  derivations must be given. Only with these
                  elements clearly defined can the type system of
                  Ptolemy II be compared to those extensively
                  studied in type theory. In this presentation we
                  introduce the Ptolemy II type system by informally
                  describing its capabilities and discussing a
                  number of practical use cases that illustrate its
                  limitations. Subsequently, we present a
                  corresponding formal specification in terms of a
                  formal syntax for Ptolemy II models and a set of
                  type judgements, which then we relate to a type
                  system known as HM(X): Hindley-Milner over a
                  constraint system. Finally, we discuss potential
                  changes to Ptolemy II type system that may be
                  worth further investigation.},
        URL = {http://chess.eecs.berkeley.edu/pubs/1036.html}
    }
    

Posted by Marten Lohstroh on 19 Nov 2013.
Groups: ptolemy
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.

Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.

©2002-2018 Chess