Abstract Compilation of Object-Oriented Languages into Coinductive CLP(X): Can Type Inference Meet Verification?

DOI10.1007/978-3-642-18070-5_3zbMath1308.68027OpenAlexW1864217700MaRDI QIDQ3067532

Ferruccio Damiani, Giovanni Lagorio, Davide Ancona, Andrea Corradi

Publication date: 21 January 2011

Published in: Formal Verification of Object-Oriented Software (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-18070-5_3

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Theory of programming languages (68N15) Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (2)

Idealized coinductive type systems for imperative object-oriented programs ⋮ Abstract Compilation of Object-Oriented Languages into Coinductive CLP(X): Can Type Inference Meet Verification?

Uses Software

• Featherweight Java

Cites Work

• Fundamental properties of infinite trees
• Intersection and union types: Syntax and semantics
• Idealized coinductive type systems for imperative object-oriented programs
• Abstract Compilation of Object-Oriented Languages into Coinductive CLP(X): Can Type Inference Meet Verification?
• Verifying Complex Continuous Real-Time Systems with Coinductive CLP(R)
• Type Inference by Coinductive Logic Programming
• Constraint Handling Rules
• Co-Logic Programming: Extending Logic Programming with Coinduction
• Coinductive Logic Programming
• HM(X) type inference is CLP(X) solving

This page was built for publication: Abstract Compilation of Object-Oriented Languages into Coinductive CLP(X): Can Type Inference Meet Verification?