Expressive power of typed and type-free programming languages
type: Item
instance of: scholarly article
title: Expressive power of typed and type-free programming languages
zbMATH Open document ID: 0557.68022
DOI: 10.1016/0304-3975(84)90088-4
author: Elfriede Fehr
published in: Theoretical Computer Science
publication date: 1984-01-01T00:00:00Z
review text: The paper investigates the influence of type-free programming concepts on the definability of functions and objects in comparison with the exclusive use of typed concepts plus fixed-point operators. The underlying schemes are the classes of type-free and typed lambda-schemes respectively. The formal semantics of both classes are analyzed in the same semantical domains. In particular it is shown that typed lambda- schemes are translatable into equivalent type-free lambda-schemes but not vice verse. Furthermore, it is proved that the class of type-free lambda- schemes is universal in the sense that in the initial models all recursively enumerable \(\Sigma\)-trees (where \(\Sigma\) is the set of operation symbols) are definable.
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68N01
Mathematics Subject Classification ID: 03D60
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 68Q65
zbMATH DE Number: 3888902
zbMATH Keywords: type theory
zbMATH Keywords: lambda-calculus
zbMATH Keywords: type-free programming concepts
zbMATH Keywords: typed lambda-schemes
zbMATH Keywords: formal semantics
describes a project that uses: ALGOL 60
describes a project that uses: ALGOL 68
describes a project that uses: LCF
MaRDI profile type: Publication
full work available at URL: 0304-3975(84)90088-4
OpenAlex ID: W2081900912
cites work: A draft description of Pascal
cites work: Least fixed points revisited
cites work: Q5649409
cites work: A global representation of the recursive functions in the \(\lambda\)- calculus
cites work: The lambda calculus, its syntax and semantics
cites work: Q4160405
cites work: Q3205213
cites work: Q5531462
cites work: Q4068081
cites work: Q4109650
cites work: Q5618896
cites work: On Classes of Program Schemata
cites work: Q5565113
cites work: Combinatory logic. Vol. II
cites work: Q4172933
cites work: Q4151140
cites work: Q4156412
cites work: Simple program schemes and formal languages
cites work: IO and OI. II
cites work: Q4070302
cites work: Q3904045
cites work: Initial Algebra Semantics and Continuous Algebras
cites work: Theory of program structures: Schemes, semantics, verification
cites work: Q4163516
cites work: Q5686017
cites work: Q3681911
cites work: Q5592246
cites work: Q4101793
cites work: Q4070337
cites work: Q4105238
cites work: Q4766569
cites work: Correspondence between ALGOL 60 and Church's Lambda-notation
cites work: On procedures as open subroutines. II
cites work: Q5636311
cites work: Q4101795
cites work: Q4174202
cites work: Q4766020
cites work: Algebraic automata and context-free sets
cites work: Q4133080
cites work: Q4138713
cites work: Fully abstract models of typed \(\lambda\)-calculi
cites work: λ-definierbare Funktionen auf Peanoalgebren
cites work: The Standardization Theorem for λ‐Calculus
cites work: Q4124819
cites work: Q4116078
cites work: Q4185781
cites work: LCF considered as a programming language
cites work: Q5573961
cites work: Q5649639
cites work: Data Types as Lattices
cites work: Q5685626
cites work: The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty $-Models of the Lambda-Calculus
cites work: Approximate Reduction and Lambda Calculus Models
cites work: Q4182475

Expressive power of typed and type-free programming languages (cites work)
cites work: The programming language Pascal