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

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