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
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, Types for ambient and process mobility, 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
