Functional Characters of Solvable Terms
From MaRDI portal
Publication:3936713
DOI10.1002/malq.19810270205zbMath0479.03006OpenAlexW2119240423MaRDI QIDQ3936713
Mario Coppo, Betti Venneri, Mariangiola Dezani-Ciancaglini
Publication date: 1981
Published in: Mathematical Logic Quarterly (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1002/malq.19810270205
typesfunctionalitylambda calculus languagenatural deduction systems with introduction and elimination rulesnonsignificant expressionsnormal form of a term
Related Items (57)
Adding algebraic rewriting to the calculus of constructions : Strong normalization preserved ⋮ \(F\)-semantics for type assignment systems ⋮ On sets of terms having a given intersection type ⋮ Intersection types and lambda models ⋮ Principality and type inference for intersection types using expansion variables ⋮ A characterization of F-complete type assignments ⋮ Intersection type assignment systems ⋮ Unnamed Item ⋮ Nominal essential intersection types ⋮ Type theories, normal forms, and \(D_{\infty}\)-lambda-models ⋮ A resource aware semantics for a focused intuitionistic calculus ⋮ The ``relevance of intersection and union types ⋮ Meeting of the Association for Symbolic Logic, Stanford, California, 1985 ⋮ Strong normalization and typability with intersection types ⋮ Semantic types and approximation for Featherweight Java ⋮ Intersection and union types ⋮ The coherence of languages with intersection types ⋮ Type Inference for Rank 2 Gradual Intersection Types ⋮ Typed generic traversal with term rewriting strategies ⋮ Structural rules and algebraic properties of intersection types ⋮ Applicative intersection types ⋮ Node Replication: Theory And Practice ⋮ Non-idempotent intersection types in logical form ⋮ Disjoint Polymorphism ⋮ Calculi, types and applications: essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi della Rocca ⋮ On strong normalization and type inference in the intersection type discipline ⋮ A type assignment system for game semantics ⋮ A Type Theory for Probabilistic $$\lambda $$–calculus ⋮ Approximation Semantics and Expressive Predicate Assignment for Object-Oriented Programming ⋮ Strong normalization through intersection types and memory ⋮ Type reconstruction in finite rank fragments of the second-order \(\lambda\)-calculus ⋮ Complete restrictions of the intersection type discipline ⋮ Intersection types for combinatory logic ⋮ Types with intersection: An introduction ⋮ Hyperformulae, Parallel Deductions and Intersection Types ⋮ Intersection Types and Computational Rules ⋮ A filter lambda model and the completeness of type assignment ⋮ The bang calculus revisited ⋮ The emptiness problem for intersection types ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Strictness, totality, and non-standard-type inference ⋮ Completeness of intersection and union type assignment systems for call-by-value \(\lambda\)-models ⋮ Completeness of type assignment systems with intersection, union, and type quantifiers ⋮ Reasoning About Call-by-need by Means of Types ⋮ Typing and computational properties of lambda expressions ⋮ Typing untyped \(\lambda\)-terms, or reducibility strikes again! ⋮ Normalization without reducibility ⋮ Principal type schemes for an extended type theory ⋮ Normalization, approximation, and semantics for combinator systems ⋮ Intersection and singleton type assignment characterizing finite Böhm-trees ⋮ Simple type-theoretic foundations for object-oriented programming ⋮ Taming the Merge Operator ⋮ Essential and relational models ⋮ Elaborating intersection and union types ⋮ Full abstraction for lambda calculus with resources and convergence testing
This page was built for publication: Functional Characters of Solvable Terms
