Kripke models and the (in)equational logic of the second-order \(\lambda\)-calculus
type: Item
instance of: scholarly article
title: Kripke models and the (in)equational logic of the second-order \(\lambda\)-calculus
zbMATH Open document ID: 0873.03017
DOI: 10.1016/S0168-0072(96)00039-5
published in: Annals of Pure and Applied Logic
publication date: 1997-06-16T00:00:00Z
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 18D15
Mathematics Subject Classification ID: 03G30
zbMATH DE Number: 1022205
zbMATH Keywords: Kripke models
zbMATH Keywords: rewrite rules
zbMATH Keywords: second-order \(\lambda\)-calculus
zbMATH Keywords: soundness
zbMATH Keywords: completeness
zbMATH Keywords: proof systems
zbMATH Keywords: inequalities
zbMATH Keywords: equations
zbMATH Keywords: category of preorders
zbMATH Keywords: exponential of functors
zbMATH Keywords: Cartesian-closed category
zbMATH Keywords: type abstraction
author: Jean Gallier
MaRDI profile type: Publication
cites work: Extensional models for polymorphism
cites work: Q4068706
cites work: The system \({\mathcal F}\) of variable types, fifteen years later
cites work: Q3962973
cites work: Q4288818
cites work: Completeness in the theory of types
cites work: Filter models with polymorphic types
cites work: Sheaves in geometry and logic: a first introduction to topos theory
cites work: Kripke-style models for typed lambda calculus
cites work: Q3786612
cites work: Q3922646
cites work: A semantics for static type inference
cites work: Categorical semantics for higher order polymorphic lambda calculus
cites work: Completeness, invariance and λ-definability
full work available at URL: s0168-0072(96)00039-5
OpenAlex ID: W1985397485
description: scientific article; zbMATH DE number 1022205