296 research outputs found
Pure Type Systems without Explicit Contexts
No full textContains fulltext :
84166.pdf (Author’s version preprint ) (Open Access)LFMTP 201
Substructural Parametricity
No full textOrdered, linear, and other substructural type systems allow us to expose deep properties of programs at the syntactic level of types. In this paper, we develop a family of unary logical relations that allow us to prove consequences of parametricity for a range of substructural type systems. A key idea is to parameterize the relation by an algebra, which we exemplify with a monoid and commutative monoid to interpret ordered and linear type systems, respectively. We prove the fundamental theorem of logical relations and apply it to deduce extensional properties of inhabitants of certain types. Examples include demonstrating that the ordered types for list append and reversal are inhabited by exactly one function, as are types of some tree traversals. Similarly, the linear type of the identity function on lists is inhabited only by permutations of the input. Our most advanced example shows that the ordered type of the list fold function is inhabited only by the fold function
Admissibility of fixpoint induction over partial types
No full textPartial types allow the reasoning about partial functions in type theory. The partial functions of main interest are recursively computed functions, which are commonly assigned types using xpoint induction. However, xpoint induction is valid only on admissible types. Previous work has shown manytypes to be admissible, but has not shown any dependent products to be admissible. Disallowing recursion on dependent product types substantially reduces the expressiveness of the logic; for example, it prevents much reasoning about modules, objects and algebras. In this paper I present two new tools, predicate-admissibility and monotonicity, for showing types to be admissible. These tools show a wide class of types to be admissible; in particular, they show many dependent products to be admissible. This alleviates di culties in applying partial types to theorem proving in practice. I also present a general least upper bound theorem for xed points with regard to a computational approximation relation, and show an elegant application of the theorem to compactness. This research was conducted while the author was at Cornell University. This material is based on work supported in part by ARPA/AF grant F30602-95-1-0047, and AASERT grant N00014-95-1-0985. Any opinions, ndings, and conclusions or recommendations expressed in this publication are those of the author and do not re ect the views of these agencies
La camera obscura, au-delà du “dispositif foucaldien” proposé par Jonathan Crary dans L’art de l’observateur
No full textTechniques of the Observer by Jonathan Crary became a reference text in the field of the studies of the optical devices from the point of view of the espistemology. But the approach very influenced by Michel Foucault of the devices, in particular of the camera obscura, leads the author to privilege the sociology to the detriment of the aesthetics, and can ask question
La camera obscura, au-delà du “dispositif foucaldien” proposé par Jonathan Crary dans L’art de l’observateur
No full textL’Art de l’observateur de Jonathan Crary est devenu un texte de référence dans le domaine des études sur les dispositifs optiques du point de vue de l’épistémologie. Pour autant, l’approche très foucaldienne des appareils, en particulier de la camera obscura, conduit l’auteur à privilégier les aspects sociologiques au détriment de l’esthétique, et peut poser question.Techniques of the Observer by Jonathan Crary became a reference text in the field of the studies of the optical devices from the point of view of the espistemology. But the approach very influenced by Michel Foucault of the devices, in particular of the camera obscura, leads the author to privilege the sociology to the detriment of the aesthetics, and can ask question
Simple, Efficient Object Encoding using Intersection Types
No full textI present a type-theoretic encoding of objects that interprets method dispatch by self-application (i.e., method functions are applied to the objects containing them) but still validates the expected subtyping relationships. The naive typing of self-application fails to validate the expected subtyping relationships because it is too permissive and allows application to similarly typed objects that are not self. This new encoding solves this problem by constraining methods to be applied only to self using existential and intersection types. Using this typing, I give a full account of objects including self types and method update. The typing constructs used in this encoding appear to be quite rich, but they may be axiomatized in a novel, restricted fashion that is metatheoretically simple. This research was sponsored by the Advanced Research Projects Agency CSTO under the title "The Fox Project: Advanced Languages for Systems Software", ARPA Order No. C533, issued by ESC/ENS under Contr..
Toward a practical type theory for recursive modules
No full textModule systems for languages with complex type systems, such as Standard ML, often lack the ability to express mutually recursive type and function dependencies across module boundaries. Previous work by Crary, Harper and Puri [5] set out a type-theoretic foundation for recursive modules in the context of a phase-distinction calculus for higher-order modules. Two constructs were introduced for encoding recursive modules: a fixed-point module and a recursively dependent signature. Unfortunately, the implementations of both constructs involve the use of equi-recursive type constructors at higher-order kinds, the equivalence of which is not known to be decidable. In this paper, we show that the practicality of recursive modules is not contingent upon that of equi-recursive constructors. We begin with the theoretical infrastructure described above and study precisely how equi-recursiveness is used in the recursive module constructs, resulting in a clarification and generalization of the underlying ideas. We then examine in depth how the recursive module constructs in the revised type system can serve as the target of elaboration for a recursive module extension to Standard ML
Type-Theoretic Methodology for Practical Programming Languages
No full textThe significance of type theory to the theory of programming languages has long been recognized. Advances in programming languages have often derived from understanding that stems from type theory. However, these applications of type theory to practical programming languages have been indirect; the differences between practical languages and type theory have prevented direct connections between the two. This dissertation presents systematic techniques directly relating practical programming languages to type theory. These techniques allow programming languages to be interpreted in the rich mathematical domain of type theory. Such interpretations lead to semantics that are at once denotational and operational, combining the advantages of each, and they also lay the foundation for formal verification of computer programs in type theory. Previous type theories either have not provided adequate expressiveness to interpret practical languages, or have provided such expressiveness at the expense of essential features of the type theory. In particular, no previous type theory has supported a notion of partial functions (needed to interpret recursion in practical languages), and a notion of total functions and objects (needed to reason about data values), and an intrinsic notion of equality (needed for most interesting results). This dissertation presents the first type theory incorporating all three, and discusses issues arising in the design of that type theory. This type theory is used as the target of a type-theoretic semantics for a expressive programming calculus. This calculus may serve as an internal language for a variety of functional programming languages. The semantics is stated as a syntax-directed embedding of the programming calculus into type theory. A critical point arising in both the type theory and the type-theoretic semantics is the issue of admissibility. Admissibility governs what types it is legal to form recursive functions over. To build a useful type theory for partial functions it is necessary to have a wide class of admissible types. In particular, it is necessary for all the types arising in the type-theoretic semantics to be admissible. In this dissertation I present a class of admissible types that is considerably wider than any previously known class
A Syntactic Account of Singleton Types via Hereditary Substitution
No full textWe give a syntactic proof of decidability and consistency
of equivalence for the singleton type calculus, which lies at
the foundation of modern module systems such as that of
ML. Unlike existing proofs, which work by constructing a
model, our syntactic proof makes few demands on the underlying
proof theory and mathematical foundation. Consequently,
it can be | and has been | entirely formulated
in the Twelf meta-logic, and provides an important piece of
a Twelf-formalized type-safety proof for Standard ML.
The proof works by translation of the singleton type calculus
into a canonical presentation, adapted from work on
logical frameworks, in which equivalent terms are written
identically. Canonical forms are not preserved under standard
substitution, so we employ an alternative definition of
substitution called hereditary substitution, which contracts
redices that arise during substitution
Programming Language Semantics in Foundational Type Theory
No full textThere are compelling benefits to using foundational type theory as a framework for programming language semantics. I give a semantics of an expressive programming calculus in the foundational type theory of Nuprl. Previous type-theoretic semantics have used less expressive type theories, or have sacrificed important programming constructs such as recursion and modules. The primary mechanisms of this semantics for the core calculus are partial types, for typing recursion, set types, for encoding power and singleton kinds, which are used for subtyping and module programming, and very dependent function types, for encoding signatures. I then extend the semantics to modules using phase-splitting
- …
