1 problem

0 votes0 replies0 views
Principal-type interpretation conjecture for closed beta-normal lambda-terms
Let $(\mathscr{A},{\preccurlyeq},{\to})$ be an implicative structure, and interpret closed $\lambda$ -terms and their types in a polymorphic type system with binary intersections. A…
Conjectureopenimplicative-algebras intersection-types realizabilityarXiv posted 2 days ago

Principal-type interpretation conjecture for closed beta-normal lambda-terms