Introduction to generalized type systems

DOI10.1017/S0956796800020025zbMATH Open0931.03019OpenAlexW2402296188WikidataQ63090394 ScholiaQ63090394MaRDI QIDQ4939697FDOQ4939697

Authors: Henk Barendregt 

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

Recommendations

• Introduction to Type Theory
• scientific article; zbMATH DE number 960927
• scientific article; zbMATH DE number 4126684
• scientific article; zbMATH DE number 827981
• Types for Proofs and Programs
• Specifying type systems
• Generative type abstraction and type-level computation
• scientific article; zbMATH DE number 1302061
• A new look at generalized rewriting in type theory
• Type inference for pure type systems

zbMATH Keywords

typed lambda calculi\(\lambda\)-cubeexploration of the propositions-as-types paradigmgeneral product typesgeneric calculus

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Semantics in the theory of computing (68Q55)

Cited In (42)

• Singleton, union and intersection types for program extraction
• Title not available (Why is that?)
• Title not available (Why is that?)
• Higher-order pattern anti-unification in linear time
• A unified approach to type theory through a refined \(\lambda\)-calculus
• Strong normalization in type systems: A model theoretical approach
• Mechanized metatheory revisited
• The variable containment problem
• Typed $\lambda$-calculi with one binder
• LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners
• An induction principle for pure type systems
• A syntactic proof of the conservativity of \(\lambda_\omega\) over \(\lambda_2\)
• An intuitionistic set-theoretical model of fully dependent CC
• Term-Generic Logic
• The Girard-Reynolds isomorphism (second edition)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Type-specialized staged programming with process separation
• Comprehensive Parametric Polymorphism: Categorical Models and Type Theory
• Executable Relational Specifications of Polymorphic Type Systems Using Prolog
• A Rewriting Logic Approach to Type Inference
• Closure under alpha-conversion
• Representing proof transformations for program optimization
• The Girard-Reynolds isomorphism
• A typed \(\lambda\)-calculus for proving-by-example and bottom-up generalization procedure
• Checking algorithms for Pure Type Systems
• Title not available (Why is that?)
• Modularity of termination and confluence in combinations of rewrite systems with λω
• A note on the proof theory of the \(\lambda \Pi\)-calculus
• Unified Syntax with Iso-types
• Comparing cubes of typed and type assignment systems
• The undecidability of pattern matching in calculi where primitive recursive functions are representable
• Specifying type systems
• A semantic framework for proof evidence
• Proof certificates for equality reasoning
• On functions and types: a tutorial
• The calculus of constructions as a framework for proof search with set variable instantiation
• Title not available (Why is that?)
• The expansion postponement in pure type systems
• An algorithm for checking incomplete proof objects in type theory with localization and unification
• Classical \(F_{\omega}\), orthogonality and symmetric candidates

This page was built for publication: Introduction to generalized type systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4939697)