We present a type theory combining both linearity and dependency by stratifying typing rules into a level for logics and a level for programs. The distinction between logics and programs decouples their semantics, allowing the semantics to be independently tailored to suit the needs of theorem proving and programming. A natural notion of irrelevancy is established where all proofs and types occurring inside programs are fully erasable without compromising their operational behavior. Through a heap-based operational semantics, we show that extracted programs always make computational progress and run memory clean without the need for runtime garbage collection. Additionally, programs can be freely lifted into the logical level for conducting deep proofs in the style of standard dependent type theories. This enables one to write resource-safe programs and verify their correctness using a unified language.

We present ATS/PML, a modeling language with an expressive type system (supporting both dependent types and linear types), and argue that the types in ATS/PML can be of great help in detecting modeling errors at compile-time. On one hand, we introduce modeling primitives with well-designed types into ATS/PML to facilitate a synergic combination of type-checking with model-checking. On the other hand, we compile ATS/PML into Promela so that the SPIN modelchecker can be readily employed to perform checking on models constructed in ATS/PML.

Many runtime verification tools are built based on Aspect-Oriented Programming (AOP) tools, most often AspectJ, a mature implementation of AOP for Java. Although already popular in the Java domain, there is few work on runtime verification of C programs via AOP, due to the lack of a solid language and tool support. In this paper, we propose a new general purpose and expressive language for defining monitors as an extension to the C language, and present our tool implementation of the weaver, the Movec compiler, which brings fully-fledged parametric runtime verification support into the C domain. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Runtime monitoring can be used to verify, enforce and control the dynamic execution of a target program at runtime to detect property violations, enforce desired properties and actively correct the execution, respectively. However, the state-of-the-art study lacks an appropriate formal program semantics of runtime monitoring. In this paper, we propose a theory of runtime control at an appropriate level of formalization to provide a formal program semantics of instrumented target programs under the control of controlling programs. Our theory provides a complete formal semantics for real implementations of runtime monitoring and control, but still retains a good balance between implementation and generality. Indeed, the theory encompasses the formalization of key implementation techniques, such as program instrumentation, synchronization on passively monitored actions, and synthesis of controlling programs from specifications. On the other hand, the theory is so generic and expressive that many existing formalisms about runtime monitoring can be considered as special cases of our theory.

Abstract We present an approach to enriching the type system of ML with a restricted form of dependent types, where type index terms are required to be drawn from a given type index language ${\cal L}$ that is completely separate from run-time programs, leading to the DML( ${\cal L}$ ) language schema. This enrichment allows for specification and inference of significantly more precise type information, facilitating program error detection and compiler optimization. The primary contribution of the paper lies in our language design, which can effectively support the use of dependent types in practical programming. In particular, this design makes it both natural and straightforward to accommodate dependent types in the presence of effects such as references and exceptions.

Distributed meta-programming (DMP), which allows code to be generated and distributed at run-time, has already become a common practice. However, code generation currently often relies on rather ad hoc approaches that represent code as plain text, making DMP notoriously error-prone. This unfortunate situation is further exacerbated due to issues such as mobility (of code) and locality and heterogeneity (of resources), which complicate testing and debugging drastically.In this paper, we study distributed meta-programming from a type-theoretic perspective, presenting a language to facilitate the construction of programs that may generate and distribute code at run-time. The approach we take makes use of a form of typeful code representation developed in a previous study on meta-programming, and it guarantees statically that only well-typed code (according to some chosen type discipline) can be constructed at run-time and sent to proper locations for execution. We also mention a prototype implementation in support of the practicality of our approach to DMP, providing a solid proof of concept.

1. Introduction The notion of type equality plays a pivotal r^ole in type systemdesign. However, the importance of this role is often less evident in commonly studied type systems. For instance, in the simplytyped

By allowing the programmer to write code that can generate code at run-time, meta-programming offers a powerful approach to program construction. For instance, meta-programming can often be employed to enhance program efficiency and facilitate the construction of generic programs. However, meta-programming, especially in an untyped setting, is notoriously error-prone. In this paper, we aim at making meta-programming less error-prone by providing a type system to facilitate the construction of correct meta-programs. We first introduce some code constructors for constructing typeful code representation in which program variables are represented in terms of deBruijn indexes, and then formally demonstrate how such typeful code representation can be used to support meta-programming. With our approach, a particular interesting feature is that code becomes first-class values, which can be inspected as well as executed at run-time. The main contribution of the paper lies in the recognition and then the formalization of a novel approach to typed meta-programming that is practical, general and flexible.

By allowing the programmer to write code that can generate code at run-time, meta-programming offers a powerful approach to program construction. For instance, meta-programming can often be employed to enhance program efficiency and facilitate the construction of generic programs. However, meta-programming, especially in an untyped setting, is notoriously error-prone. In this paper, we aim at making meta-programming less error-prone by providing a type system to facilitate the construction of correct meta-programs. We first introduce some code constructors for constructing typeful code representation in which program variables are replaced with deBruijn indices, and then formally demonstrate how such typeful code representation can be used to support meta-programming. The main contribution of the paper lies in recognition and then formalization of a novel approach to typed meta-programming that is practical, general and flexible.

The notion of program transformation is ubiquitous in programming language studies on interpreters, compilers, partial evaluators, etc. In order to implement a program transformation, we need to choose a representation in the meta language, that is, the programming language in which we construct programs, for representing object programs, that is, the programs in the object language on which the program transformation is to be performed. In practice, most representations chosen for typed object programs are typeless in the sense that the type of an object program cannot be reflected in the type of its representation. This is unsatisfactory as such typeless representations make it impossible to capture in the type system of the meta language various invariants in a program transformation that are related to the types of object programs. In this paper, we propose an approach to implementing program transformations that makes use of a first-order typeful program representation formed in Dependent ML (DML), where the type of an object program as well as the types of the free variables in the object program can be reflected in the type of the representation of the object program. We introduce some programming techniques needed to handle this typeful program representation, and then present an implementation of a CPS transform function where the relation between the type of an object program and that of its CPS transform is captured in the type system of DML. In a broader context, we claim to have taken a solid step along the line of research on constructing certifying compilers.

We introduce a notion of guarded recursive (g.r.) datatype constructors, generalizing the notion of recursive datatypes in functional programming languages such as ML and Haskell.

The use of types in capturing program invariants is overwhelming in practical programming. The type systems in languages such as ML and Java scale convincingly to realistic programs but they are of relatively limited expressive power. In this paper, we show that the use of restricted form of dependent types can enable us to capture many more program invariants such as memory safety while retaining practical type-checking. The programmer can encode program invariants with type annotations and then verify these invariants through static type-checking. Also, the type annotations can serve as informative program documentation, which are mechanically verified and can thus be fully trusted. We argue with realistic examples that this restricted form of dependent types can significantly facilitate program verification as well as program documentation.

We present a dependently typed assembly language (DTAL) in which the type system supports the use of a restricted form of dependent types, reaping some benefits of dependent types at the assembly level. DTAL improves upon TAL , enabling certain important compiler optimizations such as run-time array bound check elimination and tag check elimination. Also, DTAL formally addresses the issue of representing sum types at assembly level, making it suitable for handling not only datatypes in ML but also dependent datatypes in Dependent ML (DML).

Program termination verification is a challenging research subject of significant practical importance. While there is already a rich body of literature on this subject, it is still undeniably a difficult task to design a termination checker for a realistic programming language that supports general recursion. In this paper, we present an approach to program termination verification that makes use of a form of dependent types developed in Dependent ML (DML), demonstrating a novel application of such dependent types to establishing a liveness property. We design a type system that enables the programmer to supply metrics for verifying program termination and prove that every well-typed program in this type system is terminating. We also provide realistic examples, which are all verified in a prototype implementation, to support the effectiveness of our approach to program termination verification as well as its unobtrusiveness to programming. The main contribution of the paper lies in the design of an approach to program termination verification that smoothly combines types with metrics, yielding a type system capable of guaranteeing program termination that supports a general form of recursion (including mutual recursion), higher-order functions, algebraic data types and polymorphism.

The article enriches imperative programming with a form of dependent types. We start by explaining some motivations for this enrichment and mentioning some major obstacles that need to be overcome. We then present the design of a source level dependently typed imperative programming language Xanadu, forming both static and dynamic semantics and then establishing the type soundness theorem. We also present realistic examples, which have all been verified in a prototype implementation, in support of the practicality of Xanadu. We claim that the language design of Xanadu is novel and it serves as an informative example that demonstrates a means to combine imperative programming with dependent types.

We present an approach to enriching the type system of ML with a restricted form of dependent types, where type index objects are drawn from a constraint domain C, leading to the DML(C) language schema. This allows specification and inference of significantly more precise type information, facilitating program error detection and compiler optimization. A major complication resulting from introducing dependent types is that pure type inference for the enriched system is no longer possible, but we show that type-checking a sufficiently annotated program in DML(C) can be reduced to constraint satisfaction in the constraint domain C. We exhibit the unobtrusiveness of our approach through practical examples and prove that DML(C) is conservative over ML. The main contribution of the paper lies in our language design, including the formulation of type-checking rules which makes the approach practical. To our knowledge, no previous type system for a general purpose programming language such as ML has combined dependent types with features including datatype declarations, higher-order functions, general recursions, let-polymorphism, mutable references, and exceptions. In addition, we have finished a prototype implementation of DML(C) for an integer constraint domain C, where constraints are linear inequalities (Xi and Pfenning 1998).

Abstract We present a new proof for the standardization theorem in λ-calculus, which is largely built upon a structural induction on λ-terms. We then extract some bounds for the number of β-reduction steps in the standard β-reduction sequence obtained from transforming a given β-reduction sequence, sharpening the standardization theorem. As an application, we establish a super exponential bound for the lengths of β-reduction sequences from any given simply typed λ-terms.

We present a type-based approach to eliminating array bound checking and list tag checking by conservatively extending Standard ML with a restricted form of dependent types. This enables the programmer to capture more invariants through types while type-checking remains decidable in theory and can still be performed efficiently in practice. We illustrate our approach through concrete examples and present the result of our preliminary experiments which support support the feasibility and effectiveness of our approach.