Sciweavers

Share
warning: Creating default object from empty value in /var/www/modules/taxonomy/taxonomy.module on line 1416.
JFP
2002
116views more  JFP 2002»
11 years 7 months ago
Recursive subtyping revealed
Algorithms for checking subtyping between recursive types lie at the core of many programming language implementations. But the fundamental theory of these algorithms and how they...
Vladimir Gapeyev, Michael Y. Levin, Benjamin C. Pi...
ENTCS
2007
92views more  ENTCS 2007»
11 years 8 months ago
A Duality in Proof Systems for Recursive Type Equality and for Bisimulation Equivalence on Cyclic Term Graphs
This paper is concerned with a proof-theoretic observation about two kinds of proof systems for regular cyclic objects. It is presented for the case of two formal systems that are...
Clemens Grabmayer
ENTCS
2007
109views more  ENTCS 2007»
11 years 8 months ago
Constructive Membership Predicates as Index Types
In the constructive setting, membership predicates over recursive types are inhabited by terms indexing the elements that satisfy the criteria for membership. In this paper, we mo...
James Caldwell, Josef Pohl
ENTCS
2006
118views more  ENTCS 2006»
11 years 8 months ago
An Operational Domain-theoretic Treatment of Recursive Types
We develop a domain theory for treating recursive types with respect to contextual equivalence. The principal approach taken here deviates from classical domain theory in that we ...
Weng Kin Ho
CTCS
1987
Springer
11 years 11 months ago
A Typed Lambda Calculus with Categorical Type Constructors
A typed lambda calculus with categorical type constructors is introduced. It has a uniform category theoretic mechanism to declare new types. Its type structure includes categoric...
Tatsuya Hagino
POPL
1991
ACM
11 years 11 months ago
Subtyping Recursive Types
We investigate the interactions of subtyping and recursive types, in a simply typed λ-calculus. The two fundamental questions here are whether two (recursive) types are in the su...
Roberto M. Amadio, Luca Cardelli
LICS
2000
IEEE
11 years 11 months ago
Efficient and Flexible Matching of Recursive Types
Equality and subtyping of recursive types have been studied in the 1990s by Amadio and Cardelli; Kozen, Palsberg, and Schwartzbach; Brandt and Henglein; and others. Potential appl...
Jens Palsberg, Tian Zhao
ESOP
2006
Springer
11 years 11 months ago
Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types
We present a sound and complete proof technique, based on syntactic logical relations, for showing contextual equivalence of expressions in a -calculus with recursive types and imp...
Amal J. Ahmed
TLCA
1993
Springer
12 years 5 days ago
Recursive Types Are not Conservative over F
d abstract) Giorgio Ghelli1 F≤ is a type system used to study the integration of inclusion and parametric polymorphism. F≤ does not include a notion of recursive types, but ext...
Giorgio Ghelli
LICS
1999
IEEE
12 years 11 days ago
Type Inference for Recursive Definitions
We consider type systems that combine universal types, recursive types, and object types. We study type inference in these systems under a rank restriction, following Leivant'...
A. J. Kfoury, Santiago M. Pericás-Geertsen
books