Rewrites as Terms through Justification Logic

BARENBAUM, PABLO; EDUARDO BONELLI

Bologna

Conferencia; Principles and Practice of Declarative Programming; 2020

Justification Logic is a refinement of modal logic where the modality□A is annotated with a reason s for ?knowing? A and written ⟦s⟧A.The expression s is a proof of A that may be encoded as a lambdacalculus term of type A, according to the propositions-as-typesinterpretation. Our starting point is the observation that terms oftype ⟦s⟧A are reductions between lambda calculus terms. Reductionsare usually encoded as rewrites essential tools in analyzing thereduction behavior of lambda calculus and term rewriting systems,such as when studying standardization, needed strategies, Lévypermutation equivalence, etc. We explore a new propositions-as-types interpretation for Justification Logic, based on the principlethat terms of type ⟦s⟧A are proof terms encoding reductions (withsource s). Note that this provides a logical language to reason aboutrewrites.