-
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.
-
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.
-
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.
-
Type-based compression of XML data
by C. League and K. Eng.
In Proc. Data Compression Conference,
pp. 273–282, Mar. 2007. © IEEE.
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.
The source code for the implementation described in
this paper is
available for download under the GNU General Public
License.
-
MetaOCaml server pages: web publishing as staged
computation
by C. League.
Science of Computer Programming 62(1),
September, 2006. Elsevier.
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.
The source code for the implementation described in
this paper is
available for download under the GNU General Public
License.
-
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.
-
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.
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.
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
Copyrights for published articles are generally held by the
publisher. Copies hosted on this site are the author's version
of the work. Links to the definitive published versions are
also provided.
