Inhabitation of polymorphic and existential types
type: Item
instance of: scholarly article
title: Inhabitation of polymorphic and existential types
zbMATH Open document ID: 1225.03034
author: Makoto Tatsuta
author: Ryu Hasegawa
author: Hiroshi Nakano
author: Ken-etsu Fujita
published in: Annals of Pure and Applied Logic
publication date: 2011-08-26T00:00:00Z
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 03B15
Mathematics Subject Classification ID: 03B25
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 03C10
zbMATH DE Number: 5943657
zbMATH Keywords: type theory
zbMATH Keywords: second-order logic
zbMATH Keywords: existential type
zbMATH Keywords: type inhabitation
zbMATH Keywords: quantifier elimination
zbMATH Keywords: magic formulas
zbMATH Keywords: second-order witness theorem
MaRDI profile type: Publication
full work available at URL: j.apal.2010.04.009
OpenAlex ID: W1983087803
cites work: Eigenvariables, bracketing and the decidability of positive minimal predicate logic
cites work: Q4263869
cites work: Typed Lambda Calculi and Applications
cites work: Relational Parametricity and Control
cites work: Embedding first order predicate logic in fragments of intuitionistic logic
cites work: Non-strictly positive fixed points for classical natural deduction
cites work: Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence
cites work: A simple proof of second-order strong normalization with permutative conversions
cites work: Simple Saturated Sets for Disjunction and Second-Order Existential Quantification
cites work: Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
cites work: Q4499084
cites work: Q3024919
cites work: Typability and type checking in System F are equivalent and undecidable
DOI: 10.1016/J.APAL.2010.04.009
description: scientific article; zbMATH DE number 5943657