Type reconstruction in Fω

DOI10.1017/S0960129597002302zbMath0883.03044OpenAlexW2010240397MaRDI QIDQ4347376

Paweł Urzyczyn

Publication date: 24 March 1998

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0960129597002302

zbMATH Keywords

partial recursive functionCurry styleGirard's calculus \(F_ \omega\)strongly normalizable termtype assignment system for pure lambda termstype reconstruction problem

Mathematics Subject Classification ID

Logic in computer science (03B70) Metamathematics of constructive systems (03F50) Combinatory logic and lambda calculus (03B40)

Related Items (4)

Principality and type inference for intersection types using expansion variables ⋮ A typed lambda calculus with intersection types ⋮ Typability and type checking in System F are equivalent and undecidable ⋮ Alpha-conversion and typability

This page was built for publication: Type reconstruction in F_ω