The Principal Type-Scheme of an Object in Combinatory Logic
From MaRDI portal
Publication:5592242
DOI10.2307/1995158zbMath0196.01501OpenAlexW4249075482WikidataQ56518660 ScholiaQ56518660MaRDI QIDQ5592242
Publication date: 1969
Published in: Transactions of the American Mathematical Society (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.2307/1995158
Related Items (76)
Simple type inference for term graph rewriting systems ⋮ Explicit effect subtyping ⋮ Higher-order unification via combinators ⋮ Polymorphic type inference with overloading and subtyping ⋮ A characterization of F-complete type assignments ⋮ The Girard-Reynolds isomorphism ⋮ Intersection type assignment systems ⋮ On the cooperation of the constraint domains ℋ, ℛ, and ℱ in CFLP ⋮ Normalization results for typeable rewrite systems ⋮ Effect-polymorphic behaviour inference for deadlock checking ⋮ Principal type scheme and unification for intersection type discipline ⋮ Polymorphic type inference and containment ⋮ A proof-centric approach to mathematical assistants ⋮ Constructive natural deduction and its ‘ω-set’ interpretation ⋮ On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory ⋮ Verification of FPGA layout generators in higher-order logic ⋮ Size-based termination of higher-order rewriting ⋮ The Girard-Reynolds isomorphism (second edition) ⋮ Semantic types and approximation for Featherweight Java ⋮ Type inference in polymorphic type discipline ⋮ Principal type-schemes of BCI-lambda-terms ⋮ Trends in trends in functional programming 1999/2000 versus 2007/2008 ⋮ Type Inference for Rank 2 Gradual Intersection Types ⋮ Existential type systems between Church and Curry style (type-free style) ⋮ Unnamed Item ⋮ Bidirectional data flow analysis for type inferencing. ⋮ Primitive recursive functional with dependent types ⋮ In Praise of Impredicativity: A Contribution to the Formalization of Meta-Programming ⋮ Quantitative weak linearisation ⋮ Type Reconstruction for $$\lambda $$-DRT Applied to Pronoun Resolution ⋮ Coercions in a polymorphic type system ⋮ Deforestation: Transforming programs to eliminate trees ⋮ Type inference for polymorphic references ⋮ Weak polymorphism can be sound ⋮ Implementing a method for stochastization of one-step processes in a computer algebra system ⋮ Logic programs as compact denotations. ⋮ Safe functional systems through integrity types and verified assembly ⋮ Condensed detachment is complete for relevance logic: A computer-aided proof ⋮ Two beta-equal lambda-I-terms with no types in common ⋮ Type reconstruction in finite rank fragments of the second-order \(\lambda\)-calculus ⋮ Complete restrictions of the intersection type discipline ⋮ The converse principal type-scheme theorem in lambda calculus ⋮ On subsumption and semiunification in feature algebras ⋮ Constructing type systems over an operational semantics ⋮ Principal types of BCK-lambda-terms ⋮ The correctness of Newman's typability algorithm and some of its extensions ⋮ Type inference with simple subtypes ⋮ Introduction to Type Theory ⋮ Computability in higher types, P\(\omega\) and the completeness of type assignment ⋮ Type inference and strong static type checking for Promela ⋮ Strictness, totality, and non-standard-type inference ⋮ A theory of type polymorphism in programming ⋮ Visible Type Application ⋮ Formal verification of algorithm \(\mathcal{W}\): the monomorphic case ⋮ Types for ambient and process mobility ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 12--17, 2023 ⋮ COCHIS: Stable and coherent implicits ⋮ Objects and session types ⋮ Type inference with recursive types: Syntax and semantics ⋮ Extending the type checker of Standard ML by polymorphic recursion ⋮ Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages ⋮ Encoding types in ML-like languages ⋮ On the semantics of polymorphism ⋮ Weak linearization of the lambda calculus ⋮ The completeness theorem for typing lambda-terms ⋮ On principal types of combinators ⋮ Principal type schemes for an extended type theory ⋮ Typability and type checking in System F are equivalent and undecidable ⋮ Type inference for variant object types ⋮ The complexity of type inference for higher-order typed lambda calculi ⋮ Type inference for record concatenation and multiple inheritance ⋮ Definition of the semantics of programming language constructs in terms of ?-calculus. I ⋮ Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) ⋮ An NSF proposal ⋮ Refinement types for program analysis ⋮ A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
This page was built for publication: The Principal Type-Scheme of an Object in Combinatory Logic
