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