Introduction to generalized type systems
From MaRDI portal
Publication:4939697
DOI10.1017/S0956796800020025zbMath0931.03019OpenAlexW2402296188WikidataQ63090394 ScholiaQ63090394MaRDI QIDQ4939697
Publication date: 9 February 2000
Published in: Journal of Functional Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0956796800020025
typed lambda calculi\(\lambda\)-cubeexploration of the propositions-as-types paradigmgeneral product typesgeneric calculus
Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Combinatory logic and lambda calculus (03B40)
Related Items (35)
Higher-order pattern anti-unification in linear time ⋮ The Girard-Reynolds isomorphism ⋮ Strong normalization in type systems: A model theoretical approach ⋮ A note on the proof theory of the \(\lambda \Pi\)-calculus ⋮ LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners ⋮ Unified Syntax with Iso-types ⋮ A Rewriting Logic Approach to Type Inference ⋮ Term-Generic Logic ⋮ Comparing cubes of typed and type assignment systems ⋮ The expansion postponement in pure type systems ⋮ The Girard-Reynolds isomorphism (second edition) ⋮ Singleton, union and intersection types for program extraction ⋮ Type-specialized staged programming with process separation ⋮ Checking algorithms for Pure Type Systems ⋮ Closure under alpha-conversion ⋮ An intuitionistic set-theoretical model of fully dependent CC ⋮ A semantic framework for proof evidence ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Modularity of termination and confluence in combinations of rewrite systems with λω ⋮ A typed \(\lambda\)-calculus for proving-by-example and bottom-up generalization procedure ⋮ Proof certificates for equality reasoning ⋮ The variable containment problem ⋮ An algorithm for checking incomplete proof objects in type theory with localization and unification ⋮ Classical \(F_{\omega}\), orthogonality and symmetric candidates ⋮ The undecidability of pattern matching in calculi where primitive recursive functions are representable ⋮ Unnamed Item ⋮ An induction principle for pure type systems ⋮ Executable Relational Specifications of Polymorphic Type Systems Using Prolog ⋮ Representing proof transformations for program optimization ⋮ Unnamed Item ⋮ Comprehensive Parametric Polymorphism: Categorical Models and Type Theory ⋮ Mechanized metatheory revisited ⋮ A syntactic proof of the conservativity of \(\lambda_\omega\) over \(\lambda_2\) ⋮ The calculus of constructions as a framework for proof search with set variable instantiation
This page was built for publication: Introduction to generalized type systems
