Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts

DOI10.1007/s10817-006-9061-yzbMath1118.68046OpenAlexW2065324910MaRDI QIDQ2642466

Luigi Liquori, Marino Miculan, Alberto Ciaffaglione

Publication date: 17 August 2007

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-01148347/file/2007-jar-07.pdf

zbMATH Keywords

Logical frameworksInteractive theorem provingCoinductive type theoriesFunctional and imperative object-calculiLogical foundations of programming

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts ⋮ Mechanizing type environments in weak HOAS ⋮ ASP\(_{\text{fun}}\) : a typed functional active object calculus ⋮ Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax ⋮ A Mechanized Model of the Theory of Objects

Uses Software

• Coq
• KRAKATOA

Cites Work

• A new approach to abstract syntax with variable binding
• Co-induction in relational semantics
• A linear logical framework
• \(\pi\)-calculus in (Co)inductive-type theory
• On the formalization of the modal \(\mu\)-calculus in the calculus of inductive constructions
• Verified bytecode verifiers.
• The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
• Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts
• Recursion over objects of functional type
• Developing (Meta)Theory of λ-calculus in the Theory of Contexts1 1Work partially supported by Italian MURST project tosca and EC-WG types.
• A framework for defining logics
• Consistency of the theory of contexts
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item