TY - GEN
T1 - Rewrites as terms through justification logic
AU - Barenbaum, Pablo
AU - Bonelli, Eduardo
N1 - Publisher Copyright:
© 2020 ACM.
PY - 2020/9/8
Y1 - 2020/9/8
N2 - Justification Logic is a refinement of modal logic where the modality is annotated with a reason s for "knowing"A and written . The expression s is a proof of A that may be encoded as a lambda calculus term of type A, according to the propositions-as-types interpretation. Our starting point is the observation that terms of type are reductions between lambda calculus terms. Reductions are usually encoded as rewrites essential tools in analyzing the reduction behavior of lambda calculus and term rewriting systems, such as when studying standardization, needed strategies, Lévy permutation equivalence, etc. We explore a new propositions-as-types interpretation for Justification Logic, based on the principle that terms of type are proof terms encoding reductions (with source s). Note that this provides a logical language to reason about rewrites.
AB - Justification Logic is a refinement of modal logic where the modality is annotated with a reason s for "knowing"A and written . The expression s is a proof of A that may be encoded as a lambda calculus term of type A, according to the propositions-as-types interpretation. Our starting point is the observation that terms of type are reductions between lambda calculus terms. Reductions are usually encoded as rewrites essential tools in analyzing the reduction behavior of lambda calculus and term rewriting systems, such as when studying standardization, needed strategies, Lévy permutation equivalence, etc. We explore a new propositions-as-types interpretation for Justification Logic, based on the principle that terms of type are proof terms encoding reductions (with source s). Note that this provides a logical language to reason about rewrites.
KW - Curry-Howard
KW - Lambda calculus
KW - modal logic
KW - term rewriting
KW - type systems
UR - http://www.scopus.com/inward/record.url?scp=85092756308&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85092756308&partnerID=8YFLogxK
U2 - 10.1145/3414080.3414091
DO - 10.1145/3414080.3414091
M3 - Conference contribution
AN - SCOPUS:85092756308
T3 - ACM International Conference Proceeding Series
BT - Proceedings of the 22nd International Symposium on Principles and Practice of Declarative Programming, PPDP 2020 - Part of BOPL 2020 - Bologna Federated Conference on Programming Languages 2020
T2 - 22nd International Symposium on Principles and Practice of Declarative Programming, PPDP 2020 - Part of 2020 Bologna Federated Conference on Programming Languages, BOPL 2020
Y2 - 8 September 2020 through 10 September 2020
ER -