Skip to Main content Skip to Navigation
Conference papers

A Two-Level Logic Perspective on (Simultaneous) Substitutions

Kaustuv Chaudhuri 1, 2
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : Lambda-tree syntax (λts), also known as higher-order abstract syntax (hoas), is a representational technique where the pure λ-calculus in a meta language is used to represent binding constructs in an object language. A key feature of λts is that capture-avoiding substitution in the object language is represented by β-reduction in the meta language. However, to reason about the meta-theory of (simultaneous) substitutions , it may seem that λts gets in the way: not only does iterated β-reduction not capture simultaneity, but also β-redexes are not first-class constructs. This paper proposes a representation of (simultaneous) substitutions in the two-level logic approach (2lla), where properties of a specification language are established in a strong reasoning meta-logic that supports inductive reasoning. A substitution, which is a partial map from variables to terms, is represented in a form similar to typing contexts, which are partial maps from variables to types; both are first-class in 2lla. The standard typing rules for substitutions are then just a kind of context relation that are already well-known in 2lla. This representation neither changes the reasoning kernel, nor requires any modification of existing type systems, and does not sacrifice any expressivity.
Document type :
Conference papers
Complete list of metadata

Cited literature [36 references]  Display  Hide  Download

https://hal.inria.fr/hal-01968139
Contributor : Kaustuv Chaudhuri <>
Submitted on : Wednesday, January 2, 2019 - 10:28:43 AM
Last modification on : Friday, April 30, 2021 - 9:55:16 AM
Long-term archiving on: : Wednesday, April 3, 2019 - 2:51:13 PM

File

simsub_hal.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01968139, version 1

Collections

Citation

Kaustuv Chaudhuri. A Two-Level Logic Perspective on (Simultaneous) Substitutions. CPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2018, Los Angeles, United States. ⟨hal-01968139⟩

Share

Metrics

Record views

100

Files downloads

242