Journal of Functional Programming
SCOPUS (1991-2025)SCIE-ISI
1469-7653
0956-7968
Anh Quốc
Cơ quản chủ quản: Cambridge University Press , CAMBRIDGE UNIV PRESS
Lĩnh vực:
Software
Các bài báo tiêu biểu
Simple type-theoretic foundations for object-oriented programming
Tập 4 Số 2 - Trang 207-247 - 1994
AbstractWe develop a formal, type-theoretic account of the basic mechanisms of
object-oriented programming: encapsulation, message passing, subtyping and
inheritance. By modelling object encapsulation in terms of existential types
instead of the recursive records used in other recent studies, we obtain a
substantial simplification both in the model of objects and in the underlying
typed λ-calculus...
A paradigmatic object-oriented programming language: Design, static typing and semantics
Tập 4 Số 2 - Trang 127-206 - 1994
AbstractTo illuminate the fundamental concepts involved in object-oriented
programming languages, we describe the design of TOOPL, a paradigmatic,
statically-typed, functional, object-oriented programming language which
supports classes, objects, methods, hidden instance variables, subtypes and
inheritance.It has proven to be quite difficult to design such a language which
has a secure type system...
Using types as search keys in function libraries
Tập 1 Số 1 - Trang 71-89 - 1991
AbstractA method is proposed to search for an identifier in a functional program
library by using its Hindley–Milner type as a key. This can be seen as an
approximation of using the specification as a key.Functions that only differ in
their argument order or currying are essentially the same, which is expressed by
a congruence relation on types. During a library search, congruent types are
identif...
The bologna optimal higher-order machine
Tập 6 Số 6 - Trang 763-810 - 1996
AbstractThe Bologna Optimal Higher-order Machine (BOHM) is a prototype
implementation of the core of a functional language based on (a variant of)
Lamping's optimal graph reduction technique (Lamping, 1990; Gonthier et al.,
1992a; Asperti, 1994). The source language is a sugared λ-calculus enriched with
booleans, integers, lists and basic operations on these data types (following
the guidelines of...
A unifying type-theoretic framework for objects
Tập 5 Số 4 - Trang 593-635 - 1995
AbstractWe give a direct type-theoretic characterization of the basic mechanisms
of object-oriented programming, including objects, methods, message passing, and
subtyping, by introducing an explicit constructor for object types and suitable
introduction, elimination, and equality rules. The resulting abstract framework
provides a basis for justifying and comparing previous encodings of objects
ba...
Retrieving reusable software components by polymorphic type
Tập 1 Số 2 - Trang 191-211 - 1991
AbstractPolymorphic types are labels classifying both (a) defined components in
a library and (b) contexts of free variables in partially written programs. It
is proposed to help programmers make better use of software libraries by
providing a system that, given (b), identifies candidates from (a) with matching
types. Assuming at first that matching means unifying (i.e. having a common
instance), ...
FUNCTIONAL PEARL Linear lambda calculus and PTIME-completeness
Tập 14 Số 6 - Trang 623-633 - 2004
We give transparent proofs of the PTIME-completeness of two decision problems
for terms in the λ-calculus. The first is a reproof of the theorem that type
inference for the simply-typed λ-calculus is PTIME-complete. Our proof is
interesting because it uses no more than the standard combinators Church knew of
some 70 years ago, in which the terms are linear affine – each bound variable
occurs at mo...
Deciding type isomorphisms in a type-assignment framework
Tập 3 Số 4 - Trang 485-525 - 1993
AbstractThis paper provides a formal treatment of isomorphic types for languages
equipped with an ML style polymorphic type inference mechanism. The results
obtained make less justified the commonplace feeling that (the core of) ML is a
subset of second order λ-calculus: we can provide an isomorphism of types that
holds in the core ML language, but not in second order λ-calculus. This new
isomorph...