The Expressiveness of Simple and Second-Order Type Structures

DOI10.1145/322358.322370MaRDI QIDQ3668859zbMATH OpenOpenAlexWikidataFDO

Authors Steven Fortune, Daniel M. Leivant, Michael J. O'Donnell

Publication date 1983

Published in Journal of the ACM (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/322358.322370

zbMATH Keywords

normalizationpolymorphismtyped lambda calculussecond-order typestype structuresimple types

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Abstract data types; algebraic specification (68Q65)

Cited in

(38)

• A quantitative model for simply typed λ-calculus
• About primitive recursive algorithms
• Polymorphic extensions of simple type structures. With an application to a bar recursive minimization
• Proofs of strong normalisation for second order classical natural deduction
• Parameter-reduction of higher level grammars
• A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
• Iterating on multiple collections in synchrony
• Inductive types and type constraints in the second-order lambda calculus
• Automatic synthesis of typed -programs on term algebras
• A unary representation result for system \(T\)
• Finitely stratified polymorphism
• Extensional models for polymorphism
• An analysis of the Core-ML language: Expressive power and type reconstruction
• Orders, reduction graphs and spectra
• Algebraic types in PER models
• Third-order Idealized Algol with iteration is decidable
• Implicit computation complexity in higher-order programming languages
• How to prove representation-independent independence results
• Typing and computational properties of lambda expressions
• From realizability to induction via dependent intersection
• A characterization of F-complete type assignments
• Polymorphic type inference and containment
• Meeting of the Association for Symbolic Ldgic, Washington, DC, 1985
• From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models
• Informal versus formal mathematics
• The calculus of dependent lambda eliminations
• The semantics of second-order lambda calculus
• System \(T\), call-by-value and the minimum problem
• Inductively defined types in the Calculus of Constructions
• On the metamathematics of the P vs. NP question
• Investigations on the dual calculus
• Index sets and presentations of complexity classes
• On the implementation of abstract data types by programming language constructs
• Categorical data types in parametric polymorphism
• Preface to the special volume
• Type reconstruction in finite rank fragments of the second-order -calculus
• Unprovability of theorems of complexity theory in weak number theories
• Canonicity and normalization for dependent type theory

This page was built for publication: The Expressiveness of Simple and Second-Order Type Structures

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3668859)