Idealized coinductive type systems for imperative object-oriented programs

DOI10.1051/ita/2011009zbMath1220.68047MaRDI QIDQ3006157

Davide Ancona, Giovanni Lagorio

Publication date: 10 June 2011

Published in: RAIRO - Theoretical Informatics and Applications (Search for Journal in Brave)

Full work available at URL: http://www.numdam.org/item?id=ITA_2011__45_1_3_0/

zbMATH Keywords

coinduction; type analysis; imperative object-oriented languages; SSA intermediate form

Mathematics Subject Classification ID

68N19: Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)

03B70: Logic in computer science

Related Items

Union and intersection types to support both dynamic and static typing, Proof Relevant Corecursive Resolution, Abstract Compilation of Object-Oriented Languages into Coinductive CLP(X): Can Type Inference Meet Verification?, Type Inference by Coinductive Logic Programming

Uses Software

• Featherweight Java

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Coinductive big-step operational semantics
• Fundamental properties of infinite trees
• Intersection and union types: Syntax and semantics
• Abstract Compilation of Object-Oriented Languages into Coinductive CLP(X): Can Type Inference Meet Verification?
• Coinductive Logic Programming with Negation
• Verifying Complex Continuous Real-Time Systems with Coinductive CLP(R)
• Type Inference by Coinductive Logic Programming
• Co-Logic Programming: Extending Logic Programming with Coinduction
• Coinductive Logic Programming
• HM(X) type inference is CLP(X) solving