J-Calc: a typed lambda calculus for intuitionistic justification logic

DOI10.1016/j.entcs.2013.12.012zbMath1337.03023OpenAlexW2036565723WikidataQ113317925 ScholiaQ113317925MaRDI QIDQ276037

Konstantinos Pouliasis, Guiseppe Primiero

Publication date: 26 April 2016

Full work available at URL: https://doi.org/10.1016/j.entcs.2013.12.012

zbMATH Keywords

justification logicmodular programmingtyped \(\lambda\)-calculus

Mathematics Subject Classification ID

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

Related Items

Logic of Intuitionistic Interactive Proofs (Formal Theory of Perfect Knowledge Transfer) ⋮ A Curry–Howard View of Basic Justification Logic

Uses Software

• Agda

Cites Work

• The ontology of justifications in the logical setting
• The logic of proofs, semantically
• Lectures on the Curry-Howard isomorphism
• Logic of proofs
• Explicit Provability and Constructive Semantics
• A judgmental reconstruction of modal logic
• An Introduction to Gödel's Theorems
• Justification Logic
• Kripke Semantics for Martin-Löf’s Extensional Type Theory
• Dependently Typed Programming in Agda
• Contextual modal type theory
• The Intensional Lambda Calculus
• Existence and feasibility in arithmetic
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item