A Mechanized Model of the Theory of Objects

DOI10.1007/978-3-540-72952-5_12MaRDI QIDQ5428912zbMATH OpenOpenAlexFDO

Authors Ludovic Henrio, Florian Kammüller

Publication date 28 November 2007

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-72952-5_12

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Semantics in the theory of computing (68Q55)

Recommendations

• The Isabelle Framework
• scientific article; zbMATH DE number 2079996
• scientific article; zbMATH DE number 6721685
• Theoretical Aspects of Computing – ICTAC 2005
• Unifying theories of programming in Isabelle

Cites work

• A concurrent lambda calculus with futures
• A head-to-head comparison of de Bruijn indices and names
• A type-theoretic interpretation of pointcuts and advice
• Asynchronous and deterministic objects
• Automated Deduction – CADE-20
• scientific article; zbMATH DE number 1231693 (Why is no real title available?)
• scientific article; zbMATH DE number 1479620 (Why is no real title available?)
• scientific article; zbMATH DE number 2161893 (Why is no real title available?)
• scientific article; zbMATH DE number 944097 (Why is no real title available?)
• scientific article; zbMATH DE number 1860622 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• More Church-Rosser proofs (in Isabelle/HOL)
• Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts
• The lambda calculus. Its syntax and semantics. Rev. ed.

Cited in

(7)

• A graph-based implementation for mechanized refinement calculus of OO programs
• Turning Inductive into Equational Specifications
• Unifying Theories of Objects
• ASP\(_{\text{fun}}\) : a typed functional active object calculus
• scientific article; zbMATH DE number 1019597 (Why is no real title available?)
• scientific article; zbMATH DE number 2079996 (Why is no real title available?)
• Theoretical Aspects of Computing – ICTAC 2005

Describes a project that uses

Uses Software

• Nominal Isabelle

This page was built for publication: A Mechanized Model of the Theory of Objects

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