Building continuous webbed models for system F
We present here a large family of concrete models for Girard and Reynolds polymorphism (system F), in a noncategorical setting. The family generalizes the construction of the model of Barbanera and Berardi (Tech. Report, University of Turin, 1997), ...
Equilogical spaces
It is well known that one can build models of full higher-order dependent-type theory (also called the calculus of constructions) using partial equivalence relations (PERs) and assemblies over a partial combinatory algebra. But the idea of categories of ...
Two-level languages for program optimization
Two-level languages incorporate binding time information inside types, that is, whether a piece of code is completely known at compile-time, or needs some more inputs and can be evaluated only at run-time. We consider the use of 2-level languages in the ...
Poset-valued sets or how to build models for linear logics
We describe a method for constructing models of linear logic based on the category of sets and relations. The resulting categories are non-degenerate in general; in particular they are not compact closed nor do they have biproducts. The construction is ...
Real functions incrementally computable by finite automata
This is an investigation into exact real number computation using the incremental approach of Potts (Ph.D. Thesis, Department of Computing, Imperial College, 1998), Edalat and Potts (Electronic Notes in Computer Science, Vol. 6, Elsevier Science ...
The correspondence between partial metrics and semivaluations
Partial metrics, or the equivalent weightable quasi-metrics, have been introduced in Matthews (Proc. 8th Summer Conf. on General Topology and Applications; Ann. New York Acad. Sci. 728 (1994) 183) as part of the study of the denotational semantics of ...
Encoding types in ML-like languages
This article presents several general approaches to programming with type-indexed families of values within a Hindley-Milner type system. A type-indexed family of values is a function that maps a family of types to a family of values. The function ...
Minimal length test vectors for multiple-fault detection
A methodology for circuit testing is proposed for detecting multiple circuit faults in the course of a minimal length "guided tour" of the circuit transition structure. Deriving a test vector to guide this tour through an n state subsystem with at most ...
Semantic models for information flow
In the past, several definitions of information flow have been presented, based upon process algebras. Unfortunately, all these appear to be either too weak--failing to identify certain subtle forms of information flow or too strong--indicating ...
Possible worlds and resources: the semantics of BI
The logic of bunched implications, BI, is a substructural system which freely combines an additive (intuitionistic) and a multiplicative (linear) implication via bunches (contexts with two combining operations, one which admits Weakening and Contraction ...