Justification logic as a foundation for certifying mobile computation

DOI10.1016/J.APAL.2011.09.007MaRDI QIDQ408548zbMATHOpenAlexFDO

Authors Eduardo Bonelli, Federico Feller

Publication date 10 April 2012

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.apal.2011.09.007

zbMATH Keywords

justification logicCurry-de Bruijn-Howard isomorphismmobile computationtyped lambda calculus

Mathematics Subject Classification ID

Theory of programming languages (68N15) Logics of knowledge and belief (including belief change) (03B42) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Recommendations

• The Logic of Proofs as a Foundation for Certifying Mobile Computation
• Justification logic and audited computation
• Certification Using the Mobius Base Logic
• J-Calc: a typed lambda calculus for intuitionistic justification logic
• Justification logic and history based computation

Cites work

• scientific article; zbMATH DE number 2079018 (Why is no real title available?)
• scientific article; zbMATH DE number 2209442 (Why is no real title available?)
• A Constructive Logic for Services and Information Flow in Computer Networks
• A judgmental reconstruction of modal logic
• A modal analysis of staged computation
• Computer Science Logic
• Justification logic and history based computation
• Logic of proofs
• Logical Mobility and Locality Types
• Programming Languages and Systems
• The Intensional Lambda Calculus
• The Logic of Proofs as a Foundation for Certifying Mobile Computation
• The duality of computation
• Types and programing languages

Cited in

(8)

• Intuitionistic hypothetical logic of proofs
• J-Calc: a typed lambda calculus for intuitionistic justification logic
• Hypothetical logic of proofs
• The Logic of Proofs as a Foundation for Certifying Mobile Computation
• Explicit auditing
• Certification Using the Mobius Base Logic
• Strongly normalizing audited computation
• Justification logic and audited computation

Describes a project that uses

Uses Software

• MiniML

This page was built for publication: Justification logic as a foundation for certifying mobile computation

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