Skip to content
<open-source>
Oeiuwq Faith Blog OpenSource Porfolio

ernius/formalmetatheory-nominal

Alpha-Structural Induction and Recursion for the Lambda Calculus in Constructive Type Theory
Source code at GitHub http://ernius.github.io/formalmetatheory-nominal/
ernius/formalmetatheory-nominal.json
{
  "createdAt": "2015-03-27T17:55:44Z",
  "defaultBranch": "master",
  "description": "Alpha-Structural Induction and Recursion for the Lambda Calculus in Constructive Type Theory",
  "fullName": "ernius/formalmetatheory-nominal",
  "homepage": "http://ernius.github.io/formalmetatheory-nominal/",
  "language": "Agda",
  "name": "formalmetatheory-nominal",
  "pushedAt": "2018-05-06T21:02:04Z",
  "stargazersCount": 6,
  "topics": [
    "agda",
    "calculus",
    "formalisation",
    "lambda"
  ],
  "updatedAt": "2022-03-22T10:49:54Z",
  "url": "https://github.com/ernius/formalmetatheory-nominal"
}

Alpha-Structural Induction and Recursion for the Lambda Calculus in Constructive Type Theory

Section titled “Alpha-Structural Induction and Recursion for the Lambda Calculus in Constructive Type Theory”

We formulate principles of induction and recursion for a variant of lambda calculus with bound names where alpha-conversion is based upon name swapping as in nominal abstract syntax. The principles allow to work modulo alpha-conversion and apply the Barendregt variable convention. We derive them all from the simple structural induction principle and apply them to get some fundamental meta-theoretical results, such as the substitution lemma for alpha-conversion and the result of substitution composition. The whole work is implemented in Agda, and is browsable here.

Documentation

Section titled “Documentation”

Authors

Section titled “Authors”
  • Ana Bove (Chalmers University of Technology)
  • Ernesto Copello (Universidad ORT Uruguay)
  • Maribel Fernandez (King’s College London)
  • Nora Szasz (Universidad ORT Uruguay)
  • Álvaro Tasistro (Universidad ORT Uruguay)

Build Status in Travis CI : Build Status

Section titled “Build Status in Travis CI : ”

Agda compiler version 2.5.1 and standard library version 0.12

Updated version of this work:

Section titled “Updated version of this work:”

Machine-checked proof of the Church-Rosser theorem for Lambda-Calculus using the Barendregt Variable Convention in Constructive Type Theory, Electronic Notes in Theoretical Computer Science,2018 in press.

Project