scholarly journals Annotated Type Systems for Program Analysis

1995 ◽  
Vol 24 (498) ◽  
Author(s):  
Kirsten Lackner Solberg
Keyword(s):  
Program Analysis ◽  
Abstract Interpretation ◽  
Operational Semantics ◽  
Type System ◽  
Denotational Semantics ◽  
Type Systems ◽  
Strictness Analysis ◽  
Binding Time ◽  
The One ◽  
Treat All

<p>In this Ph.D. thesis, we study four program analyses. Three of them are specified by annotated type systems and the last one by abstract interpretation.</p><p>We present a combined strictness and totality analysis. We are specifying the analysis as an annotated type system. The type system allows conjunctions of annotated types, but only at the top-level. The analysis is somewhat more powerful than the strictness analysis by Kuo and Mishra due to the conjunctions and in that we also consider totality. The analysis is shown sound with respect to a natural-style operational semantics. The analysis is not immediately extendable to full conjunction.</p><p>The second analysis is also a combined strictness and totality analysis, however with ``full´´ conjunction. Soundness of the analysis is shown with respect to a denotational semantics. The analysis is more powerful than the strictness analyses by Jensen and Benton in that it in addition to strictness considers totality. So far we have only specified the analyses, however in order for the analyses to be practically useful we need an algorithm for inferring the annotated types. We construct an algorithm for the second analysis using the lazy type approach by Hankin and Le Métayer. The reason for choosing the second analysis from the thesis is that the approach is not applicable to the first analysis.</p><p>The third analysis we study is a binding time analysis. We take the analysis specified by Nielson and Nielson and we construct a more efficient algorithm than the one proposed by Nielson and Nielson. The algorithm collects constraints in a structural manner like the type inference algorithm by Damas. Afterwards the minimal solution to the set of constraints is found.</p><p>The last analysis in the thesis is specified by abstract interpretation. Hunt shows that projection based analyses are subsumed by PER (partial equivalence relation) based analyses using abstract interpretation. The PERs used by Hunt are strict, i.e. bottom is related to bottom. Here we lift this restriction by requiring the PERs to be uniform, in the sense that they treat all the integers equally. By allowing non-strict PERs we get three properties on the integers, corresponding to the three annotations used in the first and second analysis in the thesis.</p>

Phantom types and subtyping

2006 ◽  
Vol 16 (6) ◽  
pp. 751-791 ◽  
Author(s):  
MATTHEW FLUET ◽  
RICCARDO PUCELLA
Keyword(s):  
Type System ◽  
Type Systems ◽  
First Order ◽  
Standard Ml ◽  
Parametric Polymorphism ◽  
The One ◽  
Multiple Interface

We investigate a technique from the literature, called the phantom-types technique, that uses parametric polymorphism, type constraints, and unification of polymorphic types to model a subtyping hierarchy. Hindley-Milner type systems, such as the one found in Standard ML, can be used to enforce the subtyping relation, at least for first-order values. We show that this technique can be used to encode any finite subtyping hierarchy (including hierarchies arising from multiple interface inheritance). We formally demonstrate the suitability of the phantom-types technique for capturing first-order subtyping by exhibiting a type-preserving translation from a simple calculus with bounded polymorphism to a calculus embodying the type system of SML.

scholarly journals Semantics-Based Compiling: A Case Study in Type-Directed Partial Evaluation

1996 ◽  
Vol 3 (13) ◽  
Author(s):  
Olivier Danvy ◽  
René Vestergaard
Keyword(s):  
Program Analysis ◽  
Partial Evaluation ◽  
Denotational Semantics ◽  
Type Inference ◽  
Attribute Grammars ◽  
Effective Solution ◽  
Source Language ◽  
Binding Time ◽  
Genuine Solution

<p>We illustrate a simple and effective solution to semantics-based<br />compiling. Our solution is based on type-directed partial evaluation, where</p><p><br />- our compiler generator is expressed in a few lines, and is efficient; <p> - its input is a well-typed, purely functional definitional interpreter in the manner of denotational semantics;</p>- the output of the generated compiler is three-address code, in the fashion and efficiency of the Dragon Book;</p><p>- the generated compiler processes several hundred lines of source code per second.</p><p><br />The source language considered in this case study is imperative, block-structured,<br />higher-order, call-by-value, allows subtyping, and obeys<br />stack discipline. It is bigger than what is usually reported in the literature on semantics-based compiling and partial evaluation.<br />Our compiling technique uses the first Futamura projection, i.e., we compile programs by specializing a definitional interpreter with respect to this program. Our denitional interpreter is completely straightforward, stack-based, and in direct style. In particular, it requires no clever staging technique (currying, continuations, binding-time improvements, etc.), nor does it rely on any other framework (attribute grammars, annotations, etc.) than the typed lambda-calculus. In particular, it uses no other program analysis than traditional type inference. The overall simplicity and effectiveness of the approach has encouraged us to write this paper, to illustrate this genuine solution to denotational semantics-directed compilation, in the spirit of Scott and Strachey.</p>

scholarly journals Typing first-class continuations in ML

1993 ◽  
Vol 3 (4) ◽  
pp. 465-484 ◽  
Author(s):  
Robert Harper ◽  
Bruce F. Duba ◽  
David Macqueen
Keyword(s):  
Operational Semantics ◽  
Type System ◽  
Type Systems ◽  
Functional Language ◽  
Type Assignment ◽  
Polymorphic Type ◽  
Alternative Type

AbstractAn extension of ML with continuation primitives similar to those found in Scheme is considered. A number of alternative type systems are discussed, and several programming examples are given. A continuation-based operational semantics is defined for a small, purely functional language, and the soundness of the Damas–Milner polymorphic type assignment system with respect to this semantics is proved. The full Damas–Milner type system is shown to be unsound in the presence of first-class continuations. Restrictions on polymorphism similar to those introduced in connection with reference types are shown to suffice for soundness.

scholarly journals Semantic Foundations of Data Flow Analysis

1981 ◽  
Vol 10 (131) ◽  
Author(s):  
Flemming Nielson
Keyword(s):  
Program Analysis ◽  
Abstract Interpretation ◽  
Data Flow ◽  
Flow Analysis ◽  
Denotational Semantics ◽  
System Of Equations ◽  
Program Transformations ◽  
Sensitive Data ◽  
Data Flow Analysis ◽  
Made In

<p>Abstract Interpretation (P. Cousot, R. Cousot and others) is a method for program analysis that is able to describe many data flow analyses. We investigate and weaken the assumptions made in abstract interpretation and express abstract interpretation within Denotational Semantics. As an example we specify constant propagation.</p><p>Some authors have used abstract interpretation to formulate ''available expressions'' (a so-called ''history-sensitive'' data flow analysis). Our development of ''available expressions'' is better justified, semantically.</p><p>In traditional data flow analysis and abstract interpretation it is generally assumed that the ''Meet Over all Paths'' solution is wanted. We prove that the solution specified by our approach is the ''Meet Over all Paths'' solution to a certain system of equations obtained from the program.</p><p>To indicate the usefulness of our approach we show how to validate a class of program transformations, including ''constant folding''.</p><p>Throughout this paper we use a toy language consisting of declarations, expressions and commands (involving conditional and iteration). Excluded are procedures and jumps.</p>

scholarly journals Particpants' Proceedings on the Workshop: Types for Program Analysis

1995 ◽  
Vol 24 (493) ◽  
Author(s):  
Hanne Riis Nielson ◽  
Kirsten Lackner Solberg
Keyword(s):  
Programming Languages ◽  
Program Analysis ◽  
Abstract Interpretation ◽  
Recent Trend ◽  
Type Systems ◽  
Program Committee ◽  
Program Optimization ◽  
Proof Techniques ◽  
Areas Of Interest

<p>As a satellite meeting of the TAPSOFT'95 conference we organized a small workshop on program analysis. The title of the workshop, ``Types for Program Analysis´´, was motivated by the recent trend of letting the presentation and development of program analyses be influenced by annotated type systems, effect systems, and more general logical systems. The contents of the workshop was intended to be somewhat broader; consequently the call for participation listed the following areas of interest:</p><p>- specification of specific analyses for programming languages,</p><p>- the role of effects, polymorphism, conjunction/disjunction types, dependent types etc.in specification of analyses,</p><p>- algorithmic tools and methods for solving general classes of type-based analyses,</p><p>- the role of unification, semi-unification etc. in implementations of analyses,</p><p>- proof techniques for establishing the safety of analyses,</p><p>- relationship to other approaches to program analysis, including abstract interpretation and constraint-based methods,</p><p>- exploitation of analysis results in program optimization and implementation.</p><p>The submissions were not formally refereed; however each submission was read by several members of the program committee and received detailed comments and suggestions for improvement. We expect that several of the papers, in slightly revised forms, will show up at future conferences. The workshop took place at Aarhus University on May 26 and May 27 and lasted two half days.</p>

Pure iso-type systems

2019 ◽  
Vol 29 ◽  
Author(s):  
YANPENG YANG ◽  
BRUNO C. D. S. OLIVEIRA
Keyword(s):  
Operational Semantics ◽  
Type System ◽  
Type Systems ◽  
Expressive Power ◽  
Functional Languages ◽  
Type Conversion ◽  
Type Checking ◽  
Parallel Reduction ◽  
The Cost ◽  
Typed Languages

Abstract Traditional designs for functional languages (such as Haskell or ML) have separate sorts of syntax for terms and types. In contrast, many dependently typed languages use a unified syntax that accounts for both terms and types. Unified syntax has some interesting advantages over separate syntax, including less duplication of concepts, and added expressiveness. However, integrating unrestricted general recursion in calculi with unified syntax is challenging when some level of type-level computation is present, since properties such as decidable type-checking are easily lost. This paper presents a family of calculi called pure iso-type systems (PITSs), which employs unified syntax, supports general recursion and preserves decidable type-checking. PITS is comparable in simplicity to pure type systems (PTSs), and is useful to serve as a foundation for functional languages that stand in-between traditional ML-like languages and fully blown dependently typed languages. In PITS, recursion and recursive types are completely unrestricted and type equality is simply based on alpha-equality, just like traditional ML-style languages. However, like most dependently typed languages, PITS uses unified syntax, naturally supporting many advanced type system features. Instead of implicit type conversion, PITS provides a generalization of iso-recursive types called iso-types. Iso-types replace the conversion rule typically used in dependently typed calculus and make every type-level computation explicit via cast operators. Iso-types avoid the complexity of explicit equality proofs employed in other approaches with casts. We study three variants of PITS that differ on the reduction strategy employed by the cast operators: call-by-name, call-by-value and parallel reduction. One key finding is that while using call-by-value or call-by-name reduction in casts loses some expressive power, it allows those variants of PITS to have simple and direct operational semantics and proofs. In contrast, the variant of PITS with parallel reduction retains the expressive power of PTS conversion, at the cost of a more complex metatheory.

scholarly journals On the expressive power of user-defined effects: Effect handlers, monadic reflection, delimited control

2019 ◽  
Vol 29 ◽  
Author(s):  
YANNICK FORSTER ◽  
OHAD KAMMAR ◽  
SAM LINDLEY ◽  
MATIJA PRETNAR
Keyword(s):  
Operational Semantics ◽  
Type System ◽  
Denotational Semantics ◽  
Expressive Power ◽  
Programming Abstractions ◽  
Programming Abstraction ◽  
Natural Type ◽  
Inductive Types

AbstractWe compare the expressive power of three programming abstractions for user-defined computational effects: Plotkin and Pretnar’s effect handlers, Filinski’s monadic reflection, and delimited control. This comparison allows a precise discussion about the relative expressiveness of each programming abstraction. It also demonstrates the sensitivity of the relative expressiveness of user-defined effects to seemingly orthogonal language features. We present three calculi, one per abstraction, extending Levy’s call-by-push-value. For each calculus, we present syntax, operational semantics, a natural type-and-effect system, and, for effect handlers and monadic reflection, a set-theoretic denotational semantics. We establish their basic metatheoretic properties: safety, termination, and, where applicable, soundness and adequacy. Using Felleisen’s notion of a macro translation, we show that these abstractions can macro express each other, and show which translations preserve typeability. We use the adequate finitary set-theoretic denotational semantics for the monadic calculus to show that effect handlers cannot be macro expressed while preserving typeability either by monadic reflection or by delimited control. Our argument fails with simple changes to the type system such as polymorphism and inductive types. We supplement our development with a mechanised Abella formalisation.

scholarly journals Gradual session types

2019 ◽  
Vol 29 ◽  
Author(s):  
ATSUSHI IGARASHI ◽  
PETER THIEMANN ◽  
YUYA TSUDA ◽  
VASCO T. VASCONCELOS ◽  
PHILIP WADLER
Keyword(s):  
Operational Semantics ◽  
Type System ◽  
Type Systems ◽  
Session Types ◽  
Novel Approach ◽  
Seamless Transition ◽  
Linear Types ◽  
Gradual Typing ◽  
Session Type ◽  
Dynamic Typing

Abstract Session types are a rich type discipline, based on linear types, that lifts the sort of safety claims that come with type systems to communications. However, web-based applications and microservices are often written in a mix of languages, with type disciplines in a spectrum between static and dynamic typing. Gradual session types address this mixed setting by providing a framework which grants seamless transition between statically typed handling of sessions and any required degree of dynamic typing. We propose Gradual GV as a gradually typed extension of the functional session type system GV. Following a standard framework of gradual typing, Gradual GV consists of an external language, which relaxes the type system of GV using dynamic types; an internal language with casts, for which operational semantics is given; and a cast-insertion translation from the former to the latter. We demonstrate type and communication safety as well as blame safety, thus extending previous results to functional languages with session-based communication. The interplay of linearity and dynamic types requires a novel approach to specifying the dynamics of the language.

A system of constructor classes: overloading and implicit higher-order polymorphism

1995 ◽  
Vol 5 (1) ◽  
pp. 1-35 ◽  
Author(s):  
Mark P. Jones
Keyword(s):  
Type System ◽  
Type Systems ◽  
Natural Generalization ◽  
Higher Order ◽  
Functional Language ◽  
Effective Algorithm ◽  
Prototype Implementation ◽  
Type Classes

AbstractThis paper describes a flexible type system that combines overloading and higher-order polymorphism in an implicitly typed language using a system of constructor classes—a natural generalization of type classes in Haskell. We present a range of examples to demonstrate the usefulness of such a system. In particular, we show how constructor classes can be used to support the use of monads in a functional language. The underlying type system permits higher-order polymorphism but retains many of the attractive features that have made Hindley/Milner type systems so popular. In particular, there is an effective algorithm that can be used to calculate principal types without the need for explicit type or kind annotations. A prototype implementation has been developed providing, amongst other things, the first concrete implementation of monad comprehensions known to us at the time of writing.

Sign in / Sign up

Export Citation Format

Share Document