2008

1. Something for Everyone: AI Lab Assignments that Span Learning Styles and Aptitudes by C. League. Journal of Computing Sciences in Colleges 23(5), pp. 142–149, May 2008. © CCSC.

   Abstract

   One of the great challenges of teaching is managing a wide range of educational backgrounds, learning styles, aptitudes, and time/energy constraints in the same classroom. Aiming down the middle is a poor strategy; it is unacceptable to write off the lower half of a class, and we risk extinguishing the enthusiasm of the best and brightest by moving too slowly. We present a set of workbook-style lab assignments for an undergraduate course on artificial intelligence. By designing them carefully in accordance with Bloom’s taxonomy, they can span learning styles and aptitudes. With them, we hope to establish a disciplinary commons – a public repository of source code, notes, questions, and exercises.

2007

2. Schema-based compression of XML data with Relax NG by C. League and K. Eng. Journal of Computers 2(10), pp. 9–17, Dec. 2007. © Academy Publisher.

   Abstract

   The extensible markup language XML has become indispensable in many areas, but a significant disadvantage is its size: tagging a set of data increases the space needed to store it, the bandwidth needed to transmit it, and the time needed to parse it. We present a new compression technique based on the document type, expressed as a Relax NG schema. Assuming the sender and receiver agree in advance on the document type, conforming documents can be transmitted extremely compactly. On several data sets with high tag density this technique compresses better than other known XML-aware compressors, including those that consider the document type.

3. On the Construction of Convergent Transfer Subgraphs in General Labeled Directed Graphs by M. Ghriga and C. League. Congressus Numerantium 186, pp. 107–116, 2007. © Utilitas Mathematica Publishing.

   Abstract

   Let L and L′ be finite input and output alphabet sets, respectively. In a graph whose edges are labeled with input/output symbols, the transfer decision problem [Ghriga and Kabore 1999] is to determine whether there are sequences over L × L′ that guarantee transfer from a known vertex v to a destination vertex w. Convergent transfer subgraphs (CTS) are graphical representations of such sequences. This is an abstraction of the transfer of a communication protocol to a specific state for testing purposes.

   Li, Ghriga, and Kabore [2000] presented a polynomial time algorithm to solve the CTS problem for labeled directed acyclic graphs. This was reduced to a linear-time algorithm by Li [2003]. However, there are no efficient algorithms for general directed graphs. In this paper, we present an algebraic framework for the incremental construction of convergent transfer subgraphs. We shall prove composition theorems that form the basis for the practical construction of convergent transfer subgraphs over general directed graphs.

4. Type-based compression of XML data by C. League and K. Eng. In Proc. Data Compression Conference, pp. 273–282, Mar. 2007. © IEEE.

   The source code for the implementation described in this paper is available for download under the GNU General Public License.

   Abstract

   The extensible markup language XML has become indispensable in many areas, but a significant disadvantage is its size: tagging a set of data increases the space needed to store it, the bandwidth needed to transmit it, and the time needed to parse it. We present a new compression technique based on the document type, expressed as a Relax NG schema. Assuming the sender and receiver agree in advance on the document type, conforming documents can be transmitted extremely compactly. On several data sets with high tag density this technique compresses better than other known XML-aware compressors, including those that consider the document type.

2006

5. MetaOCaml server pages: web publishing as staged computation by C. League. Science of Computer Programming 62(1), September, 2006. Elsevier.

   The source code for the implementation described in this paper is available for download under the GNU General Public License.

   Abstract

   Modern dynamic web services are really computer programs. Some parts of these programs run off-line, others run server-side on each request, and still others run within the browser. In other words, web publishing is staged computation, either for better performance, or because certain resources are available in one stage but not another. Unfortunately, the various web programming languages make it difficult to spread computation over more than one stage. This is a tremendous opportunity for multi-stage languages in general, and for MetaOCaml in particular.

   We present the design of MetaOCaml Server Pages. Unlike other languages in its genre, the embedded MetaOCaml code blocks may be annotated with staging information, so that the programmer may safely and precisely control which computation occurs in which stage. A prototype web server, written in OCaml, supports web sites with both static and dynamic content. We provide several sample programs and demonstrate the performance gains won using multi-stage programming.

6. Typed compilation against non-manifest base classes by C. League and S. Monnier. Proc. Workshop on the Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS), LNCS 3956, edited by G. Barthe, B. Grégoire, M. Huisman, and J.L. Lanet, pp. 77–98, Apr. 2006. © Springer.

   Abstract

   Much recent work on proof-carrying code aims to build certifying compilers for single-inheritance object-oriented languages, such as Java or C#. Some modern object-oriented languages support compiling a derived class without complete information about its base class. This strategy — though necessary for supporting features such as mixins, traits, and first-class classes — is not well-supported by existing typed intermediate languages. We present a low-level IL with a type system based on the Calculus of Inductive Constructions. It is an appropriate target for efficient, type-preserving compilation of various forms of inheritance, even when the base class is unknown at compile time. Languages (such as Java) that do not require such flexibility are not penalized at run time.

2003

7. Type-preserving compilation of Featherweight Java by C. League, Z. Shao, and V. Trifonov. In OASIS: Foundations of Intrusion Tolerant Systems, edited by J.H. Lala, pp. 35–59, 2003. © IEEE.

   This is a republication of the 2002 TOPLAS article by the same name. The editor was our DARPA program director; this book is a collection of “seminal contributions” made in the OASIS program.

   Abstract

   We present an efficient encoding of core Java constructs in a simple, implementable typed intermediate language. The encoding, after type erasure, has the same operational behavior as a standard implementation using vtables and self-application for method invocation. Classes inherit super-class methods with no overhead. We support mutually recursive classes while preserving separate compilation. Our strategy extends naturally to a significant subset of Java, including interfaces and privacy. The formal translation using Featherweight Java allows comprehensible type-preservation proofs and serves as a starting point for extending the translation to new features. Our work provides a foundation for supporting certifying compilation of Java-like class-based languages in a type-theoretic framework.

8. Precision in practice: A type-preserving Java compiler by C. League, Z. Shao, and V. Trifonov. In Proc. Int’l Conf. on Compiler Construction, LNCS 2622, edited by G. Hedin, pp. 106–120, Apr. 2003. © Springer.

   Abstract

   Popular mobile code architectures (Java and .NET) include verifiers to check for memory safety and other security properties. Since their formats are relatively high level, supporting a wide range of source language features is awkward. Further compilation and optimization, necessary for efficiency, must be trusted. We describe the design and implementation of a fully type-preserving compiler for Java and ML. Its strongly-typed intermediate language provides a low-level abstract machine model and a type system general enough to prove the safety of a variety of implementation techniques. We show that precise type preservation is within reach for real-world Java systems.

2002

9. A Type-preserving compiler infrastructure by C. League. Ph.D. dissertation, Yale University, Dec. 2002.

   Abstract

   Many kinds of networked devices receive and execute new programs from various sources. Since we may not fully trust the producers of these programs, we must take measures to ensure that such code does not misbehave. Currently deployed mobile code formats can be checked for memory safety and other security properties, but they are relatively high-level. A type-preserving compiler generates lower-level, more optimized code that is still verifiable. This increases assurance by reducing the trusted computing base; we need not trust the compiler anymore. Moreover, lower-level representations naturally support a wider variety of source languages.

   Previous research on type-preserving compilation focused on functional languages or safe subsets of C. How to adapt this technology to more widely-used object-oriented languages was unknown. This dissertation explores techniques that enable a single strongly-typed intermediate language to certify programs in two very different programming languages: Java and ML.

   The major contribution is an efficient new encoding of object-oriented constructs into a typed intermediate language. I give a complete formal translation of a Java-like source calculus into a typed λ-calculus. I prove that both languages are sound and decidable, and that the translation preserves types.

   I also address many practical concerns, moving beyond the formal model to include most features of the Java language. To stage the translation, I developed λJVM, a novel representation of Java bytecode that is simpler to verify. I describe a prototype compiler that supports both Java and ML, sharing the same typed intermediate language, optimizers, code generator, and runtime system.

10. Type-preserving compilation of Featherweight Java by C. League, Z. Shao, and V. Trifonov. Transactions on Programming Languages and Systems 24(2), pp. 112–152, Mar. 2002. © ACM.

    Abstract

    We present an efficient encoding of core Java constructs in a simple, implementable typed intermediate language. The encoding, after type erasure, has the same operational behavior as a standard implementation using vtables and self-application for method invocation. Classes inherit super-class methods with no overhead. We support mutually recursive classes while preserving separate compilation. Our strategy extends naturally to a significant subset of Java, including interfaces and privacy. The formal translation using Featherweight Java allows comprehensible type-preservation proofs and serves as a starting point for extending the translation to new features. Our work provides a foundation for supporting certifying compilation of Java-like class-based languages in a type-theoretic framework.

2001

11. Functional Java bytecode by C. League, V. Trifonov, and Z. Shao. In Workshop on Intermediate Representation Engineering for the Java Virtual Machine, Jul. 2001.

    Abstract

    We describe the design and implementation of λJVM, a functional representation of Java bytecode that makes data flow explicit, verification simple, and that is well-suited for translation into lower-level representations such as those used in optimizing compilers. It is a good alternative to stack-based Java bytecode for virtual machines or ahead-of-time compilers which optimize methods and produce native code. We use λJVM as one component in a sophisticated type-preserving compiler for Java class files. Though our implementation is incomplete, preliminary measurements of both compile and run times are promising.

2000

12. Book review by C. League. Review of The optimal implementation of functional programming languages, by A. Asperti and S. Guerrini (Cambridge, 1998), in SIGACT News 31(2), pp. 6–9, Jun. 2000. © ACM.

13. Book review by C. League. Review of λ calculi: A guide for computer scientists, by C. Hankin (Oxford, 1994), in SIGACT News 31(1), pp. 8–13, Mar. 2000. © ACM.

14. Composite model checking: verification with type-specific symbolic representations by T. Bultan, R. Gerber, and C. League. Transactions on Software Engineering and Methodology 9(1), pp. 3–50, Jan. 2000. © ACM.

    Abstract

    In recent years, there has been a surge of progress in automated verification methods based on state exploration. In areas like hardware design, these technologies are rapidly augmenting key phases of testing and validation. To date, one of the most successful of these methods has been symbolic model checking, in which large finite-state machines are encoded into compact data structures such as binary decision diagrams (BDDs) — and are then checked for safety and liveness properties. However, these techniques have not realized the same success on software systems. One limitation is their inability to deal with infinite-state programs — even those with a single unbounded integer. A second problem is that of finding efficient representations for various variable types. We recently proposed a model checker for integer-based systems that uses arithmetic constraints as the underlying state representation. While this approach easily verified some subtle infinite-state concurrency problems, it proved inefficient in its treatment of boolean and (unordered) enumerated types — which are not efficiently representable using arithmetic constraints. In this paper we present a new technique that combines the strengths of both BDD and arithmetic constraint representations. Our composite model merges multiple type-specific symbolic representations in a single model checker. A system’s transitions and fixpoint computations are encoded using both BDD (for boolean and enumerated types), and arithmetic constraint (for integers) representations, where the choice depends on the variable types. Our composite model checking strategy can be extended to other symbolic representations provided that they support operations such as intersection, union, complement, equivalence checking, and relational image computations. We also present conservative approximation techniques for composite representations to address the undecidability of model checking on infinite-state systems. We demonstrate the effectiveness of our approach by analyzing two example systems which include a mixture of booleans, integers, and enumerated types. One of them is a requirements specification for the control software of a nuclear reactor’s cooling system, and the other one is a transport protocol specification.

1999

15. Representing Java classes in a typed intermediate language by C. League, Z. Shao, and V. Trifonov. In Proc. Int’l Conf. on Functional Programming, pp. 183–196, Sep. 1999. © ACM.

    Abstract

    We propose a conservative extension of the polymorphic λ-calculus (F-ω) as an intermediate language for compiling languages with name-based class and interface hierarchies. Our extension enriches standard F-ω with recursive types, existential types, and row polymorphism, but only ordered records with no sub-typing. Basing our language on F-ω makes it also a suitable target for translation from other higher-order languages; this enables the safe inter-operation between class-based and higher-order languages and the reuse of common type-directed optimization techniques, compiler back ends, and runtime support. We present the formal semantics of our intermediate language and illustrate its features by providing a formal translation from a subset of Java, including classes, interfaces, and private instance variables. The translation preserves the name-based hierarchical relation between Java classes and interfaces, and allows access to private instance variables of parameters of the same class as the one defining the method. It also exposes the details of method invocation and instance variable access and allows many standard optimizations to be performed on the object-oriented code.

1998

16. Implementing typed intermediate languages by Z. Shao, C. League, and S. Monnier. In Proc. Int’l Conf. on Functional Programming, pp. 313–323, Sep. 1998. © ACM.

    Abstract

    Recent advances in compiler technology have demonstrated the benefits of using strongly typed intermediate languages to compile richly typed source languages (e.g., ML). A type-preserving compiler can use types to guide advanced optimizations and to help generate provably secure mobile code. Types, unfortunately, are very hard to represent and manipulate efficiently; a naive implementation can easily add exponential overhead to the compilation and execution of a program. This paper describes our experience with implementing the FLINT typed intermediate language in the SML/NJ production compiler. We observe that a type-preserving compiler will not scale to handle large types unless all of its type-preserving stages preserve the asymptotic time and space usage in representing and manipulating types. We present a series of novel techniques for achieving this property and give empirical evidence of their effectiveness.

17. Verifying systems with integer constraints and boolean predicates: A composite approach by T. Bultan, R. Gerber, and C. League. In Proc. Symp. on Software Testing and Analysis, pp. 113–123, Mar. 1998. © ACM.

    Abstract

    Symbolic model checking has proved highly successful for large finite-state systems, in which states can be compactly encoded using binary decision diagrams (BDDs) or their variants. The inherent limitation of this approach is that it cannot be applied to systems with an infinite number of states — even those with a single unbounded integer. Alternatively, we recently proposed a model checker for integer-based systems that uses Presburger constraints as the underlying state representation. While this approach easily verified some subtle, infinite-state concurrency problems, it proved inefficient in its treatment of Boolean and (unordered) enumerated types — which possess no natural mapping to the Euclidean coordinate space. In this paper we describe a model checker which combines the strengths of both approaches. We use a composite model, in which a formula’s valuations are encoded in a mixed BDD-Presburger form, depending on the variables used. We demonstrate our technique’s effectiveness on a nontrivial requirements specification, which includes a mixture of Booleans, integers and enumerated types.

1997

18. Book review by C. League. Review of Isomorphisms of types: from λ-calculus to information retrieval and language design, by R. Di Cosmo (Birkhäuser, 1995), in SIGACT News 28(4), pp. 24–27, Dec. 1997. © ACM.