Type reconstruction in Fω

DOI10.1017/S0960129597002302MaRDI QIDQ4347376zbMATH OpenOpenAlexFDO

Authors 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

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

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 512796
• Type reconstruction in finite rank fragments of the second-order -calculus
• Type reconstruction for the linear -calculus with composite regular types
• Type reconstruction for the linear -calculus with composite and equi-recursive types
• Type Reconstruction for General Refinement Types
• scientific article; zbMATH DE number 5994829
• Towards a typed omega algebra
• The strict \(\omega\)-groupoid interpretation of type theory
• Transfinite constructions in classical type theory
• Type reconstruction with recursive types and atomic subtyping

Cited in

(11)

• Typability and type checking in System F are equivalent and undecidable
• Alpha-conversion and typability
• Principality and type inference for intersection types using expansion variables
• scientific article; zbMATH DE number 4134007 (Why is no real title available?)
• scientific article; zbMATH DE number 5994829 (Why is no real title available?)
• scientific article; zbMATH DE number 445160 (Why is no real title available?)
• scientific article; zbMATH DE number 512796 (Why is no real title available?)
• scientific article; zbMATH DE number 1086674 (Why is no real title available?)
• A type checker for a logical framework with union and intersection types (system description)
• Intersection types via finite-set declarations
• A typed lambda calculus with intersection types

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

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