Related papers: Modular Type-Safety Proofs using Dependant Types
We show how security type systems from the literature of language-based noninterference can be represented more directly as predicates defined by structural recursion on the programs. In this context, we show how our uniform syntactic…
Proof assistants and programming languages based on type theories usually come in two flavours: one is based on the standard natural deduction presentation of type theory and involves eliminators, while the other provides a syntax in…
Computer systems are so complex, so they are usually designed and analyzed in terms of layers of abstraction. Complexity is still a challenge facing logical reasoning tools that are used to find software design flaws and implementation…
Languages may encode similar meanings using different sentence structures. This makes it a challenge to provide a single set of formal rules that can derive meanings from sentences in many languages at once. To overcome the challenge, we…
Abstracting Gradual Typing (AGT) is an approach to systematically deriving gradual counterparts to static type disciplines. The approach consists of defining the semantics of gradual types by interpreting them as sets of static types, and…
Mathematical models are increasingly used in both academia and the pharmaceutical industry to understand how phenotypes emerge from systems of molecular interactions. However, their current construction as monolithic sets of equations…
Design patterns are distilled from many real systems to catalog common programming practice. However, some object-oriented design patterns are distorted or overly complicated because of the lack of supporting programming language constructs…
interpreters are tools to compute approximations for behaviors of a program. These approximations can then be used for optimisation or for error detection. In this paper, we show how to describe an abstract interpreter using the type-theory…
Dependently typed lambda calculi such as the Logical Framework (LF) are capable of representing relationships between terms through types. By exploiting the "formulas-as-types" notion, such calculi can also encode the correspondence between…
Native type systems are those in which type constructors are derived from term constructors, as well as the constructors of predicate logic and intuitionistic type theory. We present a method to construct native type systems for a broad…
Induction is the process by which we obtain predictive laws or theories or models of the world. We consider the structural aspect of induction. We answer the question as to whether we can find a finite and minmalistic set of operations on…
Synchronous programming languages emerged in the 1980s as tools for implementing reactive systems, which interact with events from physical environments and often must do so under strict timing constraints. In this report, we encode inside…
When using existing ACL2 datatype frameworks, many theorems require type hypotheses. These hypotheses slow down the theorem prover, are tedious to write, and are easy to forget. We describe a principled approach to types that provides…
We introduce judgemental theories and their calculi as a general framework to present and study deductive systems. As an exemplification of their expressivity, we approach dependent type theory and natural deduction as special kinds of…
Context: Reynolds showed us how to use continuation-passing style and defunctionalization to transform a recursive interpreter for a language into an abstract machine for programs in that language. The same techniques explain other…
Higher-order logic HOL offers a very simple syntax and semantics for representing and reasoning about typed data structures. But its type system lacks advanced features where types may depend on terms. Dependent type theory offers such a…
The difficulties of automatic extraction of definitions and methods from scientific documents lie in two aspects: (1) the complexity and diversity of natural language texts, which requests an analysis method to support the discovery of…
Dependent Object Types (DOT) is intended to be a core calculus for modelling Scala. Its distinguishing feature is abstract type members, fields in objects that hold types rather than values. Proving soundness of DOT has been surprisingly…
Predictive models are fundamental to engineering reliable software systems. However, designing conservative, computable approximations for the behavior of programs (static analyses) remains a difficult and error-prone process for modern…
We revisit occurrence typing, a technique to refine the type of variables occurring in type-cases and, thus, capturesome programming patterns used in untyped languages. Although occurrence typing was tied from its inceptionto set-theoretic…