A theory of type polymorphism in programming

DOI10.1016/0022-0000(78)90014-4zbMath0388.68003OpenAlexW2166822586WikidataQ55881388 ScholiaQ55881388MaRDI QIDQ1250704

Publication date: 1978

Published in: Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL: https://www.pure.ed.ac.uk/ws/files/15143545/1_s2.0_0022000078900144_main.pdf

Mathematics Subject Classification ID

General topics in the theory of software (68N01)

Related Items

Explicit effect subtyping, Soundness Conditions for Big-Step Semantics, Higher-Ranked Annotation Polymorphic Dependency Analysis, Operations on records, A Functional Abstraction of Typed Invocation Contexts, Applications of type theory, Types as parameters, Polymorphic type inference with overloading and subtyping, The Girard-Reynolds isomorphism, Types for modules, Type Inference for ZFH, Higher-order unification with dependent function types, Foundations of a theorem prover for functional and mathematical uses, On the cooperation of the constraint domains ℋ, ℛ, and ℱ in CFLP, A Rewriting Logic Approach to Type Inference, Types in Programming Languages, Between Modelling, Abstraction, and Correctness, Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis, Programming Combinations of Deduction and BDD-based Symbolic Calculation, Lower bounds for runtime complexity of term rewriting, Constructive natural deduction and its ‘ω-set’ interpretation, A system of constructor classes: overloading and implicit higher-order polymorphism, Ambivalent Types for Principal Type Inference with GADTs, CryptHOL: game-based proofs in higher-order logic, Size-based termination of higher-order rewriting, TPS: A theorem-proving system for classical type theory, A semantics for type checking, Guaranteeing safe destructive updates through a type system with uniqueness information for graphs, Trends in trends in functional programming 1999/2000 versus 2007/2008, Improving type error messages for generic Java, Type Inference for Rank 2 Gradual Intersection Types, Predicate logic as a modeling language: modeling and solving some machine learning and data mining problems withIDP3, Tactics for mechanized reasoning: a commentary on Milner (1984) ‘The use of machines to assist in rigorous proof’, In Praise of Impredicativity: A Contribution to the Formalization of Meta-Programming, Exponential automatic amortized resource analysis, Formal reasoning about finite-state discrete-time Markov chains in HOL, Coercions in a polymorphic type system, Correctness of compiling polymorphism to dynamic typing, No value restriction is needed for algebraic effects and handlers, Unnamed Item, Unnamed Item, Weak polymorphism can be sound, Region analysis for deductive verification of C programs, Implementing a method for stochastization of one-step processes in a computer algebra system, Operational interpretations of an extension of F_ω with control operators, Safe functional systems through integrity types and verified assembly, 1ML – Core and modules united, Étude et implémentation d'un système de déduction pour logique algorithmique, The Impact of the Lambda Calculus in Logic and Computer Science, An analysis of the Core-ML language: Expressive power and type reconstruction, Domain-Freeλµ-Calculus, Inferring Static Non-monotone Size-aware Types Through Testing, An embedding of Ruby in Isabelle, Functional Type Assignment for Featherweight Java, Checking Emptiness of Non-Deterministic Regular Types with Set Operators, <scp>OutsideIn(X)</scp>Modular type inference with local assumptions, Termination checking with types, Polymorphic type-checking for the ramified theory of types of Principia Mathematica, A liberal type system for functional logic programs, The emptiness problem for intersection types, A partial evaluator for the untyped lambda-calculus, Operations on records, Introduction to Type Theory, Defining and Executing P Systems with Structured Data in K, A type-theoretic semantics of arrays, Formal verification of tail distribution bounds in the HOL theorem prover, HM(X) type inference is CLP(X) solving, Overview of the Mathemagix Type System, Visible Type Application, COCHIS: Stable and coherent implicits, Local Theory Specifications in Isabelle/Isar, Richer types for \(Z\), HOL Zero’s Solutions for Pollack-Inconsistency, Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages, Extending Constructive Logic Negation with Types, Incorporating static analysis in a combinator-based compiler, Libraries for Generic Programming in Haskell, Encoding types in ML-like languages, A Declarative Debugging System for Lazy Functional Logic Programs, Specialisation of Higher-Order Functions for Debugging, Towards the Formal Reliability Analysis of Oil and Gas Pipelines, A logical analysis of aliasing in imperative higher-order functions, Implementing Compositional Analysis Using Intersection Types With Expansion Variables, On the semantics of polymorphism, The completeness theorem for typing lambda-terms, Source-tracking unification, Abstraction of Clocks in Synchronous Data-Flow Systems, TYPE INFERENCE FOR FIRST-CLASS MESSAGES WITH FEATURE CONSTRAINTS, A Scalable Inclusion Constraint Solver Using Unification, Towards Typed Prolog, Type-directed specialization of polymorphism., Simplifying subtyping constraints: a theory, Type inference for variant object types, A typed resolution principle for deduction with conditional typing theory, Heuristics for Safety and Security Constraints, Quantifier elimination and parametric polymorphism in programming languages, The complexity of type inference for higher-order typed lambda calculi, Polymorphic type, region and effect inference, On the formalization of gamma function in HOL, Refinement types for program analysis, Inferring program specifications in polynomial-time, Simple type inference for term graph rewriting systems, Hybrid information flow control for low-level code, Typed SLD-resolution: dynamic typing for logic programming, Constructive Many-one Reduction from the Halting Problem to Semi-unification (Extended Version), Polarized subtyping, Types, abstraction, and parametric polymorphism, part 2, A Verified LL(1) Parser Generator, A constraint-based region inference algorithm, Strictness, totality, and non-standard-type inference, Type inference for set theory, Evaluation of anonymity and confidentiality protocols using theorem proving, Operations on records, Inserting injection operations to denotational specifications, Contract-based verification of MATLAB-style matrix programs, Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation, On the existence of free models in abstract algebraic institutions, High-level modelling for typed functional programming, A characterization of F-complete type assignments, Toward formal development of programs from algebraic specifications: Implementations revisited, Efficient virtual machine support of runtime structural reflection, Quasi-varieties in abstract algebraic institutions, An algebraic semantics approach to the effective resolution of type equations, Intersection type assignment systems, Lower bounds on type checking overloading, A note on ``A simplified account of polymorphic references, Unification in combinations of collapse-free regular theories, Normalization results for typeable rewrite systems, Polymorphic typed defunctionalization and concretization, Pebble, a kernel language for modules and abstract data types, Formalization of reliability block diagrams in higher-order logic, A semantics of multiple inheritance, Effect-polymorphic behaviour inference for deadlock checking, Type checking a multithreaded functional language with session types, Principal type scheme and unification for intersection type discipline, Polymorphic type inference and containment, Comparing cubes of typed and type assignment systems, A proof-centric approach to mathematical assistants, On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory, Generalization from partial parametrization in higher-order type theory, Verification of FPGA layout generators in higher-order logic, The Girard-Reynolds isomorphism (second edition), A new generic scheme for functional logic programming with constraints, Efficient high-level parallel programming, Polymorphic syntax definition, Algebraic processing of programming languages, Indexed types, Covariant types, Abstract data type systems, Typed generic traversal with term rewriting strategies, Bidirectional data flow analysis for type inferencing., Meta-circular interpreter for a strongly typed language, An efficient interpreter for the lambda-calculus, Do-it-yourself type theory, Constructive system for automatic program synthesis, Deforestation: Transforming programs to eliminate trees, Semantics of types for database objects, Type inference for polymorphic references, The calculus of context relations, Logic programs as compact denotations., Linearity and iterator types for Gödel's system \(\mathcal T\), A rewrite-based type discipline for a subset of computer algebra, Programming with algebraic effects and handlers, Co-induction in relational semantics, Type checking with universes, Static semantics, types, and binding time analysis, Intensional computation with higher-order functions, Modularising the specification of a small database system in extended ML, On the expressive power of finitely typed and universally polymorphic recursive procedures, Towards proving type safety of .NET CIL, \(\pi\)-RED - a graph reducer for a full-fledged \(\lambda\)-calculus, A typed functional extension of logic programming, Optimal parallel algorithms for forest and term matching, The complexity of higher-order queries, Reusing and modifying rulebases by predicate substitution, Region-based memory management, Type reconstruction in finite rank fragments of the second-order \(\lambda\)-calculus, Complete restrictions of the intersection type discipline, On subsumption and semiunification in feature algebras, Towards proving type safety of \(\mathrm{C}^{\#}\), Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations, Constructing type systems over an operational semantics, Safety analysis versus type inference for partial types, An approach to completing variable names for implicitly typed functional languages, Structural types for systems of equations: type refinements for structurally dynamic first-class modular systems of equations, On the synthesis of function inverses, A language for generic programming in the large, Principal types of BCK-lambda-terms, Proofs of a set of hybrid let-polymorphic type inference algorithms, Reasoning about conditional probabilities in a higher-order-logic theorem prover, Formal reliability analysis of combinational circuits using theorem proving, The correctness of Newman's typability algorithm and some of its extensions, Computability in higher types, P\(\omega\) and the completeness of type assignment, Type inference and strong static type checking for Promela, Formalization of the standard uniform random variable, ML, The semantics of second-order lambda calculus, Recasting ML\(^{\text F}\), Type inference with recursive types: Syntax and semantics, Extending the type checker of Standard ML by polymorphic recursion, Strong normalization of \(\mathsf{ML}^{\mathsf F}\) via a calculus of coercions, Using theorem proving to verify expectation and variance for discrete random variables, Formal reliability and failure analysis of Ethernet based communication networks in a smart grid substation, MetaML and multi-stage programming with explicit annotations, Completeness of type assignment in continuous lambda models, A polymorphic type system for Prolog, Nominalization, predication and type containment, Type inference for record concatenation and multiple inheritance, Type inference with partial types, Satisfying subtype inequalities in polynomial space, A cost-effective estimation of uncaught exceptions in Standard ML programs, Annotation inference for modular checkers, A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction

Uses Software

Cites Work