scientific article
From MaRDI portal
zbMath0309.68016MaRDI QIDQ4068054
Publication date: 1974
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
Initial algebra semantics for lambda calculi, A type-directed, dictionary-passing translation of method overloading and structural subtyping in Featherweight Generic Go, The existential fragment of second-order propositional intuitionistic logic is undecidable, Constructive Many-one Reduction from the Halting Problem to Semi-unification (Extended Version), Types, abstraction, and parametric polymorphism, part 2, Unnamed Item, An induction principle for pure type systems, Operations on records, Typed equivalence, type assignment, and type containment, Automatic synthesis of typed \(\Lambda\)-programs on term algebras, A modular construction of type theories, \(F\)-semantics for type assignment systems, Explicit effect subtyping, Applications of type theory, Types as parameters, A characterization of F-complete type assignments, LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners, Higher-order unification with dependent function types, Adding algebraic rewriting to the untyped lambda calculus (extended abstract), Adequacy for a lazy functional language with recursive and polymorphic types, On completeness and cocompleteness in and around small categories, Inductive types and type constraints in the second-order lambda calculus, Pebble, a kernel language for modules and abstract data types, Bridging Curry and Church's typing style, A semantics of multiple inheritance, The calculus of constructions, Polymorphic type inference and containment, Comparing cubes of typed and type assignment systems, On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory, Unnamed Item, Type inference in polymorphic type discipline, An extension of system F with subtyping, Higher-order subtyping, Typed generic traversal with term rewriting strategies, Revisiting the notion of function, A domain-theoretic semantics of lax generic functions., Proof Assistants for Natural Language Semantics, A curry-style semantics of interaction: from untyped to second-order lazy \(\lambda\mu\)-calculus, Correctness of compiling polymorphism to dynamic typing, No value restriction is needed for algebraic effects and handlers, The IO- and OI-hierarchies, Semantics of types for database objects, A modest model of records, inheritance, and bounded quantification, Type checking and typability in domain-free lambda calculi, Between constructive mathematics and PROLOG, Recursion over realizability structures, Finitely stratified polymorphism, A typed lambda calculus with intersection types, Recursive types for Fun, Metacircularity in the polymorphic \(\lambda\)-calculus, An analysis of the Core-ML language: Expressive power and type reconstruction, A Type Theory for Probabilistic $$\lambda $$–calculus, Do judge a test by its cover. Combining combinatorial and property-based testing, Graded modal dependent type theory, POLYMORPHISM AND THE OBSTINATE CIRCULARITY OF SECOND ORDER LOGIC: A VICTIMS’ TALE, Filter models with polymorphic types, Domain-theoretical models of parametric polymorphism, Selective strictness and parametricity in structural operational semantics, inequationally, Divergence of \(F_{\leq}\) type checking, Third-order matching in the polymorphic lambda calculus, Type reconstruction in finite rank fragments of the second-order \(\lambda\)-calculus, Categorical models of polymorphism, Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations, Constructing type systems over an operational semantics, Incorporating quotation and evaluation into Church's type theory, Semantics of the typed \(\lambda\)-calculus with substitution in a cartesian closed category, Parameter-free polymorphic types, A language for generic programming in the large, Preface to the special volume, Adding algebraic rewriting to the untyped lambda calculus, Ensuring termination by typability, Monotone (co)inductive types and positive fixed-point types, A relational account of call-by-value sequentiality, Unnamed Item, A theory of type polymorphism in programming, Atomic polymorphism and the existence property, Unnamed Item, A family of syntactic logical relations for the semantics of Haskell-like languages, Unnamed Item, Extensional models for polymorphism, The semantics of second-order lambda calculus, Functorial polymorphism, Martin Hofmann's Case for Non-Strictly Positive Data Types, Typing and computational properties of lambda expressions, From constructivism to computer science, Generic constructions for behavioral specifications, On the logic of unification, Domain theoretic models of polymorphism, Refined typing to localize the impact of forced strictness on free theorems, Building continuous webbed models for system F, Encoding types in ML-like languages, Two extensions of system F with (co)iteration and primitive (co)recursion principles, Generalized filter models, The completeness theorem for typing lambda-terms, From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models, Unnamed Item, Typability and type checking in System F are equivalent and undecidable, Term-generic logic, Alpha-conversion and typability, Basic theory of \(F\)-bounded quantification., Relational interpretations of recursive types in an operational setting., Type-directed specialization of polymorphism., A sequent calculus for subtyping polymorphic types, Syntactic Logical Relations for Polymorphic and Recursive Types, Cogent: uniqueness types and certifying compilation, CPO-models for second order lambda calculus with recursive types and subtyping, Inferring program specifications in polynomial-time, A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
