Skip to content

Latest commit

 

History

History
116 lines (115 loc) · 6.18 KB

related-work.org

File metadata and controls

116 lines (115 loc) · 6.18 KB

Related Work

A Generator for Type Checkers by H. Gast

  • Provides a declarative specification language for type systems
  • Implements a proof search via unification and backtracking
  • Uses context modifiers (has one global context)
  • Has flags in typing rules to optimize proof search

Formally Specified Type Checkers for Domain Specific Languages: Experience Report by van den Brand, van der Meer, Serebrenik, Hofkamp

  • Designed for the quick prototyping of the specification language Chi 2.0, a language for describing concurrent systems.
  • Well integrated in the Chi tool-chain.
  • Typing rules are described in the MSDF format that describes typing rules in transition like format. One advantage is that cntext information are only mentioned when needed. This is great for extensibility and modularity.
  • MSDF also features module structures and imports. Judgments and related stuff are defined implicitly using the transition system.
  • MSDF is translated to Pyke. Originally Pyton was chosen as target, but Python does not feature backtracking capabilties by default (for cases in which more than one rule is applicable). Pyke has this feature and is inspired by Prolog (it uses the concet of backwardchaining rules).
  • The transformation form MSDF to Pyke is done with ASD+SDF.
  • The authors noticed that the integration in the Chi tool-chain required specific knowlege about the AST/DAST, thus protability to other languages is difficult.
  • The authors also have an interesting perspective on type systems as state machines.

Programmable Type Systems for Domain Specific Languages by Peter Thiemann

  • The type system of Haskell is extended to ensure the correct generation of HTML
  • They employ a first-order functional logic programming language at type level to express domain specific concepts

Semantics of Programming Languages: A Tool-oriented Approach by Heering, Jan and Klint, Paul

  • Observation: The fields semantics, tools and languages drifting further apart.
  • Reason: Semantics are rarely incooperated into pratical systems and hence do not influence tools and (partly) languages.
  • Solution: Generate as many language-based tools as possible form a semantic definition. The authors provide a hughe list of tools that could possibly be generated. Currently only generators for parsers and lexers are widely used. The authors have the vision of a development workbench for languages that can be used to generate most tools from a semantic definition.
  • Existing generation tools that can generate type checkers are
    • Synthesizer Generator
    • PSG
    • ASF+SDF
    • Centaur
    • Gem-Mex
  • Other tools that could potentially generate type checkers
    • SIS
    • DSP
    • GAG
    • SPS
    • MESS
    • Actress
    • Pregmatic
    • LDL
    • Eli

Should Your Specification Language Be Typed? by Lamport, Paulson

A Formal Description of a Type Checking Algorithm by Naeem, Harrison

  • Formal description of a type checker of a object oriented programming language called POOL.
  • POOL: class-based strongly typed object oriented programming language with parametric types
  • Type checking done bottom-up
  • Computing least common type for assignments

Ott: Effective tool support for the working semanticist by Swell, Nardelli, Owens, Peskine, Ridge, Sarkar, Strniska

  • Designed a meta-language to faciliate development of languages
  • This meta-language aims at concise and definitions that are easy to read/edit
  • Meta-language is divided into two languages, one is specifically desinged to describe binding constructs
  • Meta-language is compiled to proof-assistent and latex code

Automatic Generation of Object-Oriented Type Checkers

  • TyS frame work to faciliate the implementation of object type checkers
  • Language independent design patterns
  • Dynamic and static type system features
  • File with Types, subtyping relation and operation on types is processed by TyCC
  • Different output languages are supported (currently only Java)
  • API implemented in Java
  • Tested with flex, bison/yacc and ANTLR
  • Has been used for Calc, Drill, Frog, SubC and StaDyn
  • Polymorphic types and type variable are currently not supported

Strict Bidirectional Type Checking

  • Does not seem that helpfule.
  • Look into it if I have time left, or no other ideas.

Checking Algorithms for Pure Type Systems

  • This can be interesting!
  • They do not do this automatically, but the reasoning might be interessting.

Automatic Type Inference via Partial Evaluation

  • Use a prolog representation of the type system
  • Works well in syntax-directed case, may diverge otherwise because of prologs depth-first search
  • Translates prolog clauses automatically into an efficient two-phase constraint-based type inference algorithm
  • Partitioning paramter that specifies with parts should be delayed to the second phase
  • Result of the first phase can potenially be solved by e.g. datalog
  • Syntax directed typing rules produce conjucntions of constraints wether non-syntax directed typing rules produce conjunction and disjunctions and may be less efficient

Typemix: A Framework for Implementing Modular Extensible Type Systems

  • Modular framework suitable for the inclusion into extensible compilers
  • Based on the extensible compiler xoc
  • Type systems specified in xoc tend to be verbose
  • Consists of two languages scoperules and typerules
    • scoperules declare how scopes propagate
    • typerules, consist of judgments which relate nodes of the AST to values/types (inspired by JavaCop). Judgments are a set of syntax-directed rules interpreted in first-oder logic.
  • Type and scope rules are declarative, but Typmix has no support for proof assistence.

JavaCOP: Declarative Pluggable Types for Java

  • A frame work for pluggable type systems in Java
  • provides three tools
    • a declarative language for structural constraints (flow-insensitive)
    • a dataflow analysis engine for pluggable type systems
    • a test harness for pluggable type systems
  • hooks into javac, applies user defined rules are standard java type checking
  • JavaCOP cannot extend the syntax of Java