Rewrites as terms through justification logic

Pablo Barenbaum, Eduardo Bonelli

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

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.

Original languageEnglish
Title of host publicationProceedings 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
ISBN (Electronic)9781450388214
DOIs
StatePublished - 8 Sep 2020
Event22nd International Symposium on Principles and Practice of Declarative Programming, PPDP 2020 - Part of 2020 Bologna Federated Conference on Programming Languages, BOPL 2020 - Bologna, Online, Italy
Duration: 8 Sep 202010 Sep 2020

Publication series

NameACM International Conference Proceeding Series

Conference

Conference22nd International Symposium on Principles and Practice of Declarative Programming, PPDP 2020 - Part of 2020 Bologna Federated Conference on Programming Languages, BOPL 2020
Country/TerritoryItaly
CityBologna, Online
Period8/09/2010/09/20

Keywords

  • Curry-Howard
  • Lambda calculus
  • modal logic
  • term rewriting
  • type systems

Fingerprint

Dive into the research topics of 'Rewrites as terms through justification logic'. Together they form a unique fingerprint.

Cite this