In standard Java, wildcards behave like existential types: they must be opened before use in a method invocation, a process the compiler performs implicitly via capture conversion. We present Java-TX, a dialect of Java that sidesteps this existential encoding and treats wildcards as placeholders for unknown types, used directly without prior opening. This choice simplifies the type system and makes it compatible with an existing global type inference algorithm. The trade-off is that some method calls valid in standard Java become unavailable in Java-TX. In effect, we trade some of Java’s wildcard expressiveness for global type inference. We explore the metatheory of Java-TX through Featherweight Java-TX (FJ-TX), a functional core calculus for Java-TX that extends Featherweight Generic Java with our wildcard interpretation. We prove type soundness for FJ-TX. Finally, we evaluate the practical impact of omitting capture conversion by conducting a study on open-source Java projects by calculating an underapproximation of how much existing Java code is compatible with the Java-TX type system.

Session types provide a formal framework to enforce rich communication protocols, ensuring correctness properties such as type safety and deadlock freedom. However, the traditional API of functional session type systems with first-class channels often leads to problems with modularity and composability. This paper proposes a new, alternative session type API based on borrowing, embodied in the core calculus BGV. The borrowing-based API enables building modular and composable code for session type clients without imposing clutter or undue limitations. Its basis is a novel type system, founded on ordered linear typing, for functional session types with an explicit operation for splitting ownership of channels. We establish the semantics of BGV via a type-preserving translation to PGV, a deadlock-free functional session type calculus. We establish type safety and deadlock freedom for BGV by this translation. We also present an external version of BGV that supports use of borrow notation. We developed an algorithmic version of the type system that includes a mechanized verified translation from the external language to BGV. This part establishes decidable type checking.

Typestate systems are notoriously complex as they require sophisticated machinery for tracking aliasing. We propose a new, transition-oriented foundation for typestate in the setting of impure functional programming. Our approach relies on ordered types for simple alias tracking and its formalization draws on work on bunched implications. Yet, we support a flexible notion of borrowing in the presence of typestate. Our core calculus comes with a notion of resource types indexed by an ordered partial monoid that models abstract state transitions. We prove syntactic type soundness with respect to a resource-instrumented semantics. We give an algorithmic version of our type system and prove its soundness. Algorithmic typing facilitates a simple surface language that does not expose tedious details of ordered types. We implemented a typechecker for the surface language along with an interpreter for the core language.

Session types provide a principled approach to typed communication protocols that guarantee type safety and protocol fidelity. Formalizations of session-typed communication are typically based on process calculi, concurrent lambda calculi, or linear logic. An alternative model based on context-sensitive typing and typestate has not received much attention due to its apparent restrictions. However, this model is attractive because it does not force programmers into particular patterns like continuation-passing style or channel-passing style, but rather enables them to treat communication channels like mutable variables.

We propose algebraic protocols that enable the definition of protocol templates and session types analogous to the definition of domain-specific types with algebraic datatypes. Parameterized algebraic protocols subsume all regular as well as most context-free and nested session types and, at the same time, replace the expensive superlinear algorithms for type checking by a nominal check that runs in linear time. Algebraic protocols in combination with polymorphism increase expressiveness and modularity by facilitating new ways of parameterizing and composing session types.

All formalizations of session types rely on linear types for soundness as session-typed communication channels must change their type at every operation. Embedded language implementations of session types follow suit. They either rely on clever typing constructions to guarantee linearity statically, or on run-time checks that approximate linearity. We present a new language-embedded implementation of session types, which is inspired by the inversion-of-control design principle. With our approach, all application programs are intrinsically session-typed and unable to break linearity by construction. Our design relies on a tiny encapsulated library, for which linearity remains a proof obligation that can be discharged once and for all when the library is built. We demonstrate that our proposed design extends to a wide range of features of session type systems: branching, recursion, multichannel and higher-order sessions, as well as context-free sessions. The multichannel extension provides an embedded implementation of session types which guarantees deadlock freedom by construction. The development reported in this paper is fully backed by type-checked Agda code.

Java's type system mostly relies on type checking augmented with local type inference to improve programmer convenience. We study global type inference for Featherweight Generic Java (FGJ), a functional Java core language. Given generic class headers and field specifications, our inference algorithm infers all method types if classes do not make use of polymorphic recursion. The algorithm is constraint-based and improves on prior work in several respects. Despite the restricted setting, global type inference for FGJ is NP-complete.

Session types provide a typing discipline for structured communication on bidirectional channels. Context-free session types overcome the restriction to tail recursive protocols characteristic of conventional session types. This extension enables the serialization and deserialization of tree structures in a fully type-safe manner. We present the theory underlying the language FreeST 2, which features context-free session types in an extension of System F with linear types and a kinding system to distinguish message types, session types, and channel types. The system presents metatheoretical challenges which we address: contractivity in the presence of polymorphism, a non-trivial equational theory on types, and decidability of type equivalence. We also establish standard results on typing preservation, progress, and a characterization of erroneous processes.

Imperative session types provide an imperative interface to session-typed communication. In such an interface, channel references are first-class objects with operations that change the typestate of the channel. Compared to functional session type APIs, the program structure is simpler at the surface, but typestate is required to model the current state of communication throughout. Following an early work that explored the imperative approach, a significant body of work on session types has neglected the imperative approach and opts for a functional approach that uses linear types to manage channel references soundly. We demonstrate that the functional approach subsumes the early work on imperative session types by exhibiting a typing and semantics preserving translation into a system of linear functional session types. We further show that the untyped backwards translation from the functional to the imperative calculus is semantics preserving. We restrict the type system of the functional calculus such that the backwards translation becomes type preserving. Thus, we precisely capture the difference in expressiveness of the two calculi and conclude that the lack of expressiveness in the imperative calculus is largely due to restrictions imposed by its type system.

Developers are starting to write large and complex applications in TypeScript, a typed dialect of JavaScript. TypeScript applications integrate JavaScript libraries via typed descriptions of their APIs called declaration files. DefinitelyTyped is the standard public repository for these files. The repository is populated and maintained manually by volunteers, which is error-prone and time consuming. Discrepancies between a declaration file and the JavaScript implementation lead to incorrect feedback from the TypeScript IDE and, thus, to incorrect uses of the underlying JavaScript library.

Abstract C#, Dart, Pyret, Racket, TypeScript, VB: many recent languages integrate dynamic and static types via gradual typing. We systematically develop four calculi for gradual typing and the relations between them, building on and strengthening previous work. The calculi are as follows: $\lambda{B}$ , based on the blame calculus of Wadler and Findler (2009); $\lambda{C}$ , inspired by the coercion calculus of Henglein (1994); $\lambda{S}$ inspired by the space-efficient calculus of Herman, Tomb, and Flanagan (2006); and $\lambda{T}$ based on the threesome calculus of Siek and Wadler (2010). While $\lambda{B}$ and $\lambda{T}$ are little changed from previous work, $\lambda{C}$ and $\lambda{S}$ are new. Together, $\lambda{B}$ , $\lambda{C}$ , $\lambda{S}$ , and $\lambda{T}$ provide a coherent foundation for design, implementation, and optimization of gradual types. We define translations from $\lambda{B}$ to $\lambda{C}$ , from $\lambda{C}$ to $\lambda{S}$ , and from $\lambda{S}$ to $\lambda{T}$ . Much previous work lacked proofs of correctness or had weak correctness criteria; here we demonstrate the strongest correctness criterion one could hope for, that each of the translations is fully abstract. Each of the calculi reinforces the design of the others: $\lambda{C}$ has a particularly simple definition, and the subtle definition of blame safety for $\lambda{B}$ is justified by the simple definition of blame safety for $\lambda{C}$ . Our calculus

Systems programming often requires the manipulation of resources like file handles, network connections, or dynamically allocated memory. Programmers need to follow certain protocols to handle these resources correctly. Violating these protocols causes bugs ranging from type mismatches over data races to use-after-free errors and memory leaks. These bugs often lead to security vulnerabilities. While statically typed programming languages guarantee type soundness and memory safety by design, most of them do not address issues arising from improper handling of resources. An important step towards handling resources is the adoption of linear and affine types that enforce single-threaded resource usage. However, the few languages supporting such types require heavy type annotations. We present Affe, an extension of ML that manages linearity and affinity properties using kinds and constrained types. In addition Affe supports the exclusive and shared borrowing of affine resources, inspired by features of Rust. Moreover, Affe retains the defining features of the ML family: it is an impure, strict, functional expression language with complete principal type inference and type abstraction. does not require any linearity annotations in expressions and supports common functional programming idioms.

Session types have emerged as a typing discipline for communication protocols. Existing calculi with session types come equipped with many different primitives that combine communication with the introduction or elimination of the transmitted value. We present a foundational session type calculus with a lightweight operational semantics. It fully decouples communication from the introduction and elimination of data and thus features a single communication reduction, which acts as a rendezvous between senders and receivers. We achieve this decoupling by introducing label-dependent session types, a minimalist value-dependent session type system with subtyping. The system is sufficiently powerful to simulate existing functional session type systems. Compared to such systems, label-dependent session types place fewer restrictions on the code. We further introduce primitive recursion over natural numbers at the type level, thus allowing to describe protocols whose behaviour depends on numbers exchanged in messages. An algorithmic type checking system is introduced and proved equivalent to its declarative counterpart. The new calculus showcases a novel lightweight integration of dependent types and linear typing, with has uses beyond session type systems.

Session types have emerged as a powerful paradigm for structuring communication-based programs. They guarantee type soundness and session fidelity for concurrent programs with sophisticated communication protocols. As type soundness proofs for languages with session types are tedious and technically involved, it is rare to see mechanized soundness proofs for these systems.

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.

Regular expressions are part of every programmer’s toolbox. They are used for a wide variety of language-related tasks and there are many algorithms for manipulating them. In particular, matching algorithms that detect whether a word belongs to the language described by a regular expression are well explored, yet new algorithms appear frequently. However, there is no satisfactory methodology for testing such matchers. We propose a testing methodology which is based on generating positive as well as negative examples of words in the language. To this end, we present a new algorithm to generate the language described by a generalized regular expression with intersection and complement operators. The complement operator allows us to generate both positive and negative example words from a given regular expression. We implement our generator in Haskell and OCaml and show that its performance is more than adequate for testing.

Session types are a rich type discipline, based on linear types, that lift the sort of safety claims that come with type systems to communications. However, web-based applications and micro services 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 GradualGV as an extension of the functional session type system GV with dynamic types and casts. 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.

LJGS is a lightweight Java core calculus with a gradual security type system. The calculus guarantees secure information flow for sequential, class-based, typed object-oriented programming with mutable objects and virtual method calls. An LJGS program is composed of fragments that are checked either statically or dynamically. Statically checked fragments adhere to a security type system so that they incur no run-time penalty whereas dynamically checked fragments rely on run-time security labels. The programmer marks the boundaries between static and dynamic checking with casts so that it is always clear whether a program fragment requires run-time checks. LJGS requires security annotations on fields and methods. A field annotation either specifies a fixed static security level or it prescribes dynamic checking. A method annotation specifies a constrained polymorphic security signature. The types of local variables in method bodies are analyzed flow-sensitively and require no annotation. The dynamic checking of fields relies on a static points-to analysis to approximate implicit flows. We prove type soundness and non-interference for LJGS.

Session types describe structured communication on heterogeneously typed channels at a high level. Their tail-recursive structure imposes a protocol that can be described by a regular language. The types of transmitted values are drawn from the underlying functional language, abstracting from the details of serializing values of structured data types.

Proxies are the swiss army knives of object adaptation. They introduce a level of indirection to intercept select operations on a target object and divert them as method calls to a handler. Proxies have many uses like implementing access control, enforcing contracts, virtualizing resources. One important question in the design of a proxy API is whether a proxy object should inherit the identity of its target. Apparently proxies should have their own identity for security-related applications whereas other applications, in particular contract systems, require transparent proxies that compare equal to their target objects. We examine the issue with transparency in various use cases for proxies, discuss different approaches to obtain transparency, and propose two designs that require modest modifications in the JavaScript engine and cannot be bypassed by the programmer. We implement our designs in the SpiderMonkey JavaScript interpreter and bytecode compiler. Our evaluation shows that these modifications of have no statistically significant impact on the benchmark performance of the JavaScript engine. Furthermore, we demonstrate that contract systems based on wrappers require transparent proxies to avoid interference with program execution in realistic settings.

TreatJS is a language embedded, higher-order contract system for JavaScript which enforces contracts by run-time monitoring. Beyond providing the standard abstractions for building higher-order contracts (base, function, and object contracts), TreatJS's novel contributions are its guarantee of non-interfering contract execution, its systematic approach to blame assignment, its support for contracts in the style of union and intersection types, and its notion of a parameterized contract scope, which is the building block for composable run-time generated contracts that generalize dependent function contracts. TreatJS is implemented as a library so that all aspects of a contract can be specified using the full JavaScript language. The library relies on JavaScript proxies to guarantee full interposition for contracts. It further exploits JavaScript's reflective features to run contracts in a sandbox environment, which guarantees that the execution of contract code does not modify the application state. No source code transformation or change in the JavaScript run-time system is required. The impact of contracts on execution speed is evaluated using the Google Octane benchmark.

We present an untyped calculus of blame assignment for a higher-order contract system with two new operators: intersection and union. The specification of these operators is based on the corresponding type theoretic constructions. This connection makes intersection and union contracts their inevitable dynamic counterparts with a range of desirable properties and makes them suitable for subsequent integration in a gradual type system. A denotational specification provides the semantics of a contract in terms of two sets: a set of terms satisfying the contract and a set of contexts respecting the contract. This kind of specification for contracts is novel and interesting in its own right. A nondeterministic operational semantics serves as the specification for contract monitoring and for proving its correctness. It is complemented by a deterministic semantics that is closer to an implementation and that is connected to the nondeterministic semantics by simulation. The calculus is the formal basis of TJS, a language embedded, higher-order contract system implemented for JavaScript.

C#, Dart, Pyret, Racket, TypeScript, VB: many recent languages integrate dynamic and static types via gradual typing. We systematically develop three calculi for gradual typing and the relations between them, building on and strengthening previous work. The calculi are: λB, based on the blame calculus of Wadler and Findler (2009); λC, inspired by the coercion calculus of Henglein (1994); λS inspired by the space-efficient calculus of Herman, Tomb, and Flanagan (2006) and the threesome calculus of Siek and Wadler (2010). While λB is little changed from previous work, λC and λS are new. Together, λB, λC, and λS provide a coherent foundation for design, implementation, and optimisation of gradual types. We define translations from λB to λC and from λC to λS. Much previous work lacked proofs of correctness or had weak correctness criteria; here we demonstrate the strongest correctness criterion one could hope for, that each of the translations is fully abstract. Each of the calculi reinforces the design of the others: λC has a particularly simple definition, and the subtle definition of blame safety for λB is justified by the simple definition of blame safety for λC. Our calculus λS is implementation-ready: the first space-efficient calculus that is both straightforward to implement and easy to understand. We give two applications: first, using full abstraction from λC to λS to validate the challenging part of full abstraction between λB and λC; and, second, using full abstraction from λB to λS to easily establish the Fundamental Property of Casts, which required a custom bisimulation and six lemmas in earlier work.

This paper presents a new algorithm for the containment problem for extended regular expressions that contain intersection and complement operators and that range over infinite alphabets. The algorithm solves extended regular expressions inequalities symbolically by term rewriting and thus avoids the translation to an expression-equivalent automaton. Our algorithm is based on Brzozowski's regular expression derivatives and on Antimirov's term-rewriting approach to check containment. To deal with large or infinite alphabets effectively, we generalize Brzozowski's derivative operator to work with respect to (potentially infinite) representable character sets.

We develop a type theoretic specification of offline partial evaluation for the simply-typed lambda calculus in the dependently-typed programming language Agda. We establish the correctness of the specification by proving termination, typing preservation, and semantics preservation using logical relations. Typing preservation is achieved by relying on a typed syntax representation based on De Bruijn indices for the source and the target language. The full calculus contains primitive recursion on natural numbers and higher-order lifting for function, product, and sum types.

Type systems for information-flow control (IFC) are often inflexible and too conservative. On the other hand, dynamic run-time monitoring of information flow is flexible and permissive but it is difficult to guarantee robust behavior of a program. Gradual typing for IFC enables the programmer to choose between permissive dynamic checking and a predictable, conservative static type system, where needed. We propose ML-GS, a monomorphic ML core language with references and higher-order functions that implements gradual typing for IFC. This language contains security casts, which enable the programmer to transition back and forth between static and dynamic checking. In particular, ML-GS enables non-trivial casts on reference types so that a reference can be safely used everywhere in a program regardless of whether it was created in a dynamically or statically checked part of the program. The reference can be shared between dynamically and statically checked parts. We prove the soundness of the gradual security type system along with termination insensitive non-interference.

JSConTest introduced the notions of effect monitoring and dynamic effect inference for JavaScript. It enables the description of effects with path specifications resembling regular expressions. It is implemented by an offline source code transformation.

Partial evaluation distinguishes between different binding times when manipulating values in a program. A partial evaluator performs evaluation steps on values with a static binding time whereas it generates code for values with a dynamic binding time. Binding time descriptions have evolved from monolithic to fine grained, partially static data structures where different components may have different binding times.

The ability of tiny embedded devices to run large feature-rich programs is typically constrained by the amount of memory installed on such devices. Furthermore, the useful operation of these devices in wireless sensor applications is limited by their battery life. This paper presents a call stack redesign targeted at an efficient use of RAM storage and CPU cycles by a Java program running on a wireless sensor mote. Without compromising the application programs, our call stack redesign saves 30% of RAM, on average, evaluated over a large number of benchmarks. On the same set of bench-marks, our design also avoids frequent RAM allocations and deallocations, resulting in average 80% fewer memory operations and 23% faster program execution. These may be critical improvements for tiny embedded devices that are equipped with small amount of RAM and limited battery life. However, our call stack redesign is equally effective for any complex multi-threaded object oriented program developed for desktop computers. We describe the redesign, measure its performance and report the resulting savings in RAM and execution time for a wide variety of programs.

Contract monitoring for strict higher-order functional languages has an intuitive meaning, an established theoretical basis, and a standard implementation. For lazy functional languages, the situation is less clear-cut. There is no agreed-upon intended meaning or theory, and there are competing implementations with subtle semantic differences.

The ideal software contract fully specifies the behavior of an operation. Often, in particular in the context of scripting languages, a full specification may be cumbersome to state and may not even be desired. In such cases, a partial specification, which describes selected aspects of the behavior, may be used to raise the confidence in an implementation of the operation to a reasonable level.

The ability of tiny embedded devices to run large and feature-rich Java programs is typically constrained by the amount of memory installed on those devices. Furthermore, the useful operation of such devices in a wireless sensor application is limited by their battery life. We propose a garbage collection (GC) scheme called Offline GC which alleviates both these limitations. Our approach defies the current practice in which an object may be deallocated only if it is unreachable. Offline GC allows freeing an object that is still reachable but is guaranteed not to be used again in the program. Furthermore, it may deallocate an object inside a function, a loop or a block where it is last used, even if that object is assigned to a global field. This leads to a larger amount of memory available to a program.

The language JavaGI extends Java 1.5 conservatively by a generalized interface mechanism. The generalization subsumes retroactive and type-conditional interface implementations, binary methods, symmetric multiple dispatch, interfaces over families of types, and static interface methods. These features make certain coding patterns redundant, increase the expressiveness of the type system, and permit solutions to extension and integration problems with components in binary form, for which previously several unrelated extensions had been suggested. This article explains JavaGI and motivates its design. Moreover, it formalizes a core calculus for JavaGI and proves type soundness, decidability of typechecking, and determinacy of evaluation. The article also presents the implementation of a JavaGI compiler and an accompanying run-time system. The compiler, based on the Eclipse Compiler for Java, offers mostly modular static typechecking and fully modular code generation. It defers certain well-formedness checks until load time to increase flexibility and to enable full support for dynamic loading. Benchmarks show that the code generated by the compiler offers good performance. Several case studies demonstrate the practical utility of the language and its implementation.

Mnemonics is a Scala library for generating method bodies in JVM bytecode at run time. Mnemonics supports a large subset of the JVM instructions, for which the static typing of the generator guarantees the well-formedness of the generated bytecode. The library exploits a number of advanced features of Scala's type system (type inference with bounded polymorphism, implicit parameters, and reflection) to guarantee that the compiler only accepts legal combinations of instructions at compile time. Additional instructions can be supported at the price of a check at run time of the generator. In either case, bytecode verification of generated code is guaranteed to succeed.

Twilight STM enhances a transaction with twilight code that executes between the preparation to commit the transaction and its actual commit or abort. Twilight code runs irrevocably and concurrently with the rest of the program. It can detect and repair potential read inconsistencies in the state of its transaction and may thus turn a failing transaction into a successful one. Moreover, twilight code can safely use I/O operations while modifying the transactionally managed memory.

The 13th ACM SIGPLAN International Conference on Functional Programming (ICFP) was held in Victoria, British Columbia, Canada, in September 2008. Peter Thiemann chaired the program committee. After the conference, the authors of a selection of the presented papers were invited to submit extended versions of their work for this special issue of Journal of Functional Programming dedicated to ICFP 2008. All submitted papers were reviewed by at least three referees, including at least one expert, following the standard JFP procedures. In the end, four papers were accepted. These cover a broad range of topics and, taken together, we think they represent well the scope of ICFP 2008.

Generalized interfaces are an extension of the interface concept found in object-oriented languages such as Java or C#. The extension is inspired by Haskell's type classes. It supports retroactive and type-conditional interface implementations, binary methods, symmetric multimethods, interfaces over families of types, and static interface methods.

Current parser generators are based on context-free grammars. Because such grammars lack abstraction facilities, the resulting specifications are often not easy to read. Fischer's macro grammars extend context-free grammars with macro-like productions thus providing the equivalent of procedural abstraction. However, their use is hampered by the lack of an efficient, off-the-shelf parsing technology for macro grammars.

Correct handling of concurrently accessed external resources is a demanding problem in programming. The standard approaches rely on database transactions or concurrency mechanisms like locks. The paper considers two such resources, global variables and databases, and defines transactional APIs for them in Haskell. The APIs provide a novel flavor of user-level transactions which are particularly suitable in the context of web-based systems. This suitability is demonstrated by providing a second implementation in the context of WASH, a Haskell-based Web programming system. The underlying implementation framework works for both kinds of resources and can serve as a blueprint for further implementations of user-level transactions. The Haskell type system provides an encapsulation of the transactional scope that avoids unintended breakage of the transactional guarantees.

Modern applications are designed in multiple tiers to separate concerns. Since each tier may run at a separate location, middleware is required to mediate access between tiers. However, introducing this middleware is tiresome and error-prone.We propose a multi-tier calculus and a splitting transformation to address this problem. The multi-tier calculus serves as a sequential core programming language for constructing a multi-tier application. The application can be developed in the sequential setting. Splitting extracts one process per tier from the sequential program such that their concurrent execution behaves like the original program.The splitting transformation starts from an assignment of primitive operations to tiers. A program analysis determines communication requirements and inserts remote procedure calls. The next transformation step performs resource pooling: it optimizes the communication behavior by transforming sequences of remote procedure calls to a stream-based protocol. The final transformation step splits the resulting program into separate communicating processes.The multi-tier calculus is also applicable to the construction of interactive Web applications. It facilitates their development by providing a uniform programming framework for client-side and server-side programming.

WASH/CGI is an embedded domain-specific language for server-side Web scripting. Due to its reliance on the strongly typed, purely functional programming language Haskell as a host language, it is highly flexible and---at the same time---it provides extensive guarantees due to its pervasive use of type information.WASH/CGI can be structured into a number of sublanguages addressing different aspects of the application. The document sublanguage provides tools for the generation of parameterized XHTML documents and forms. Its typing guarantees that almost all generated documents are valid XHTML documents. The session sublanguage provides a session abstraction with a transparent notion of session state and allows the composition of documents and Web forms to entire interactive scripts. Both are integrated with the widget sublanguage which describes the communication (parameter passing) between client and server. It imposes a simple type discipline on the parameters that guarantees that forms posted by the client are always understood by the server. That is, the server never asks for data not submitted by the client and the data submitted by the client has the type requested by the server. In addition, parameters are received in their typed internal representation, not as strings. Finally, the persistence sublanguage deals with managing shared state on the server side as well as individual state on the client side. It presents shared state as an abstract data type, where the script can control whether it wants to observe mutations due to concurrently executing scripts. It guarantees that states from different interaction threads cannot be confused.

No abstract available.

Modern programming languages rely on advanced type systems that detect errors at compile-time. While the benefits of type systems have long been recognized, there are some areas where the standard systems in programming languages are not expressive enough. Language designers usually trade expressiveness for decidability of the type system. Some interesting programs will always be rejected (despite their semantical soundness) or be assigned uninformative types.

We present a framework for offline partial evaluation for call-by-value functional programming languages with an ML-style typing discipline. This includes a binding-time analysis which is (1) polymorphic with respect to binding times; (2) allows the use of polymorphic recursion with respect to binding times; (3) is applicable to a polymorphically typed term; and (4) is proven correct with respect to a novel small-step specialization semantics.The main innovation is to build the analysis on top of the region calculus of Tofte and Talpin [1994], thus leveraging the tools and techniques developed for it. Our approach factorizes the binding-time analysis into region inference and a subsequent constraint analysis. The key insight underlying our framework is to consider binding times as properties of regions.Specialization is specified as a small-step semantics, building on previous work on syntactic-type soundness results for the region calculus. Using similar syntactic proof techniques, we prove soundness of the binding-time analysis with respect to the specializer. In addition, we prove that specialization preserves the call-by-value semantics of the region calculus by showing that the reductions of the specializer are contextual equivalences in the region calculus.

Caching of documents is an important concern on the Web. It is a major win in all situations where bandwidth is limited. Unfortunately, the increasing spread of dynamically generated documents seriously hampers traditional caching techniques in browsers and on proxy servers.WASH/CGI is a Haskell-based domain specific language for creating interactive Web applications. The Web pages generated by a WASH/CGI application are highly dynamic and cannot be cached with traditional means.We show how to implement the dynamic caching scheme of the BigWig language [2] in the context of WASH/CGI. The main issue in BigWig's caching scheme is the distinction between fixed parts (that should be cached) and variable parts (that need not be cached) of a document. Since BigWig is a standalone domain-specific language, its compiler can perform the distinction as part of its static analysis. Hence, the challenge in our implementation is to obtain the same information without involving the compiler. To this end, we extend WASH/CGI's document language by mode annotations and define the translation of the resulting annotated document language into JavaScript.To alleviate the awkwardness of programming directly in annotated language, we have defined a surface syntax in the style of HSP (Haskell Server Pages) [11].

We propose a type system for locating the source of type errors in an applied lambda calculus with ML-style polymorphism. The system is based on discriminative sum types---known from work on soft typing---with annotation subtyping and recursive types. This way, type clashes can be registered in the type for later reporting. The annotations track the potential producers and consumers for each value so that clashes can be traced to their cause.Every term is typeable in our system and type inference is decidable. A type derivation in our system describes all type errors present in the program, so that a principal derivation yields a principal description of all type errors present. Error messages are derived from completed type derivations. Thus, error messages are independent of the particular algorithm used for type inference, provided it constructs such a derivation.

Execution monitoring is a proven tool for securing program execution and to enforce safety properties on applets and mobile code, in particular. Inlining monitoring tools perform their task by inserting certain run-time checks into the monitored application before executing it. For efficiency reasons, they attempt to insert as few checks as possible using techniques ranging from simple ad hoc optimizations to theorem proving. Partial evaluation is a powerful tool for specifying and implementing program transformations. The present work demonstrates that standard partial evaluation techniques are sufficient to transform an interpreter equipped with monitoring code into a non-standard compiler. This compiler generates application code, which contains the inlined monitoring code. If the monitor is enforcing a security policy, then the result is a secured application code. If the policy is defined using a security automaton, then the transformation can elide many run-time checks by using abstract interpretation. Our approach relies on proper staging of the monitoring interpreter. The transformation runs in linear time, produces code linear in the size of the original program, and is guaranteed not to duplicate incoming code.

Gifford and others proposed an effect typing discipline to delimit the scope of computational effects within a program, while Moggi and others proposed monads for much the same purpose. Here we marry effects to monads, uniting two previously separate lines of research. In particular, we show that the type, region, and effect system of Talpin and Jouvelot carries over directly to an analogous system for monads, including a type and effect reconstruction algorithm. The same technique should allow one to transpose any effect system into a corresponding monad system.

We propose an extension of Haskell's type class system with lambda abstractions in the type language. Type inference for our extension relies on a novel constrained unification procedure called guided higher-order unification. This unification procedure is more general than Haskell's kind-preserving unification but less powerful than full higher-order unification.The main technical result is the soundness and completeness of the unification rules for the fragment of lambda calculus that we admit on the type level.

Functional logic overloading is a novel approach to user-defined overloading that extends Haskell's concept of type classes in significant ways. Whereas type classes are conceptually predicates on types in standard Haskell, they are type functions in our approach. Thus, we can base type inference on the evaluation of functional logic programs. Functional logic programming provides a solid theoretical foundation for type functions and, at the same time, allows for programmable overloading resolution strategies by choosing different evaluation strategies for functional logic programs. Type inference with type functions is an instance of type inference with constrained types, where the underlying constraint system is defined by a functional logic program. We have designed a variant of Haskell which supports our approach to overloading, and implemented a prototype front-end for the language.

We define a family of embedded domain specific languages for generating HTML and XML documents. Each language is implemented as a combinator library in Haskell. The generated HTML/XML documents are guaranteed to be well-formed. In addition, each library can guarantee that the generated documents are valid XML documents to a certain extent (for HTML only a weaker guarantee is possible). On top of the libraries, Haskell serves as a meta language to define parameterized documents, to map structured documents to HTML/XML, to define conditional content, or to define entire web sites. The combinator libraries support element-transforming style , a programming style that allows programs to have a visual appearance similar to HTML/XML documents, without modifying the syntax of Haskell.

The combination of modern programming languages and partial evaluation yields new approaches to old problems. In particular, the combination of functional programming and partial evaluation can turn a general parser into a parser generator. We use an inherently functional approach to implement general LR( k ) parsers and specialize them with respect to the input grammars using offline partial evaluation. The functional specification of LR parsing yields a concise implementation of the algorithms themselves. Furthermore, we demonstrate the elegance of the functional approach by incorporating on-the-fly attribute evaluation for S-attributed grammars and two schemes for error recovery, which lend themselves to natural and elegant implementation. The parser require only minor changes to achieve good specialization results. The generated parsers have production quality and match those produced by traditional parser generators in sped and compactness

We present a general method to transform a compositional specification of a specializer for a functional programming language into a set of combinators that can be used to perform the same specialization more efficiently. The main transformation steps are the transition to higher-order abstract syntax and untagging. All transformation steps are proved correct. The resulting combinators can be implemented in any functional language, typed or untyped, pure or impure. They may also be considered as forming a domain-specific language for meta-programming. We demonstrate the generality of the method by applying it to several specializers of increasing strength. We demonstrate its efficiency by comparing it with a traditional specialization system based on self-application.

In standard control-flow analyses for higher-order languages, a single abstract binding for a variable represents a set of exact bindings, and a single abstract reference cell represents a set of exact reference cells. While such analyses provide useful may-alias information, they are unable to answer mustalias questions about variables and cells, as these questions ask about equality of specific bindings and references.In this paper, we present a novel program analysis for higher-order languages that answers must-alias questions. At every program point, the analysis associates with each variable and abstract cell a cardinality, which is either single or multiple. If variable x is single at program point p, then all bindings for x in the heap reachable from the environment at p hold the same value. If abstract cell r is single at p, then at most one exact cell corresponding to r is reachable from the environment at p.Must-alias information facilitates various program optimizations such as lightweight closure conversion [19]. In addition, must-alias information permits analyses to perform strong updates [3] on abstract reference cells known to be single. Strong updates improve analysis precision for programs that make significant use of state.A prototype implementation of our analysis yields encouraging results. Over a range of benchmarks, our analysis classifies a large majority of the variables as single.

We extend type specialisation to a computational lambda calculus with first-class references. The resulting specialiser has been used to specialise a self-interpreter for this typed computational lambda calculus optimally. Furthermore, this specialiser can perform operations on references at specialisation time, when possible.

One of the flagship applications of partial evaluation is compilation and compiler generation. However, partial evaluation is usually expressed as a source-to-source transformation for high-level languages, whereas realistic compilers produce object code.We close this gap by composing a partial evaluator with a compiler by automatic means. Our work is a successful application of several meta-computation techniques to build the system, both in theory and in practice. The composition is an application of deforestation or fusion.The result is a run-time code generation system built from existing components. Its applications are numerous. For example, it allows the language designer to perform interpreter-based experiments with a source-to-source version of the partial evaluator before building a realistic compiler which generates object code automatically.

The construction of flexible tools is a promising area for applications of functional programming. The educational tool Ebnf2ps is a medium-scale real world program that translates grammars into syntax diagrams. Its distinguishing feature is its grammar transformation mechanism, which generates highly readable output even from LALR grammars. It is therefore applicable to automatically generate documentation for the input language of parsers developed with popular parser generators, such as yacc, bison, and Happy. Ebnf2ps owes its existence–specifically the transformation feature–to its implementation language, Haskell. ©1997 by John Wiley & Sons, Ltd

We have designed and implemented a program-generator generator (PGG) for an untyped higher-order functional programming language. The program generators perform continuation-based multi-level offline specialization and thus combine the most powerful and general offline partial evaluation techniques. The correctness of the PGG is ensured by deriving it from a multi-level specialize. Our PGG is extremely simple to implement due to the use of multi-level techniques and higher-order abstract syntax.

Two key steps in the compilation of strict functional languages are the conversion of higher-order functions to data structures (closures) and the transformation to tail-recursive style. We show how to perform both steps at once by applying first-order offline partial evaluation to a suitable interpreter. The resulting code is easy to transliterate to low-level C or native code. We have implemented the compilation to C; it yields a performance comparable to that of other modern Scheme-to-C compilers. In addition, we have integrated various optimizations such as constant propagation, higher-order removal, and arity raising simply by modifying the underlying interpreter. Purely first-order methods suffice to achieve the transformations. Our approach is an instance of semantics-directed compiler generation.

Partial evaluation can turn a general parser into a parser generator.The generated parsers surpass those produced by traditional parser generators in speed and compactness.We use an inherently functional approach to implement general LR(k) parsers and specialize them using the partial evaluator Similix.The functional implementation of LR parsing allows for concise implementation of the algorithms themselves and requires only straightforward changes to achieve good specialization results.In contrast, a traditional, stack-based implementation of a general LR parser requires significant structural changes to make it amenable to satisfactory specialization.

We present an analysis to find those parts of data structures that can be modified without causing side effects.The analysis is composed of several non-standard semantics that are abstract ed to yield backward analyses.The information is gathered in a final variable oriented pass through the program.The analysis is defined for a first-order functional language with algebraic data types, and then extended to higher-order languages.As an application we give a safety analysis that determines the applicability of sr-compilation for a function.1