Type-and-scope safe programs and their proofs

Guillaume Allais, James Chapman, Conor McBride, James McKinna

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

10 Citations (Scopus)

Abstract

We abstract the common type-and-scope safe structure fromcomputations on lambda-terms that deliver, e.g., renaming, substitution, evaluation, CPS-transformation, and printing witha name supply. By exposing this structure, we can prove generic simulation and fusion lemmas relating operations built this way. This work has been fully formalised in Agda.
LanguageEnglish
Title of host publicationCPP 2017
Subtitle of host publicationProceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs
EditorsYves Bertot, Viktor Vafeiadis
Place of PublicationNew York
Number of pages13
DOIs
Publication statusPublished - 16 Jan 2017
Event6th ACM SIGPLAN Conference on Certified Programs and Proofs - Paris, France
Duration: 16 Jan 201717 Jan 2017
Conference number: 6th
http://cpp2017.mpi-sws.org/index.html

Conference

Conference6th ACM SIGPLAN Conference on Certified Programs and Proofs
Abbreviated titleCPP 2017
CountryFrance
CityParis
Period16/01/1717/01/17
Internet address

Fingerprint

Printing
Substitution reactions
Fusion reactions

Keywords

  • agda
  • dependently typed functional type
  • formal verification
  • lambda calculus
  • normalization by evaluation
  • syntax
  • semantics
  • mechanized meta theory
  • generic programming

Cite this

Allais, G., Chapman, J., McBride, C., & McKinna, J. (2017). Type-and-scope safe programs and their proofs. In Y. Bertot, & V. Vafeiadis (Eds.), CPP 2017 : Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs New York. https://doi.org/10.1145/3018610.3018613
Allais, Guillaume ; Chapman, James ; McBride, Conor ; McKinna, James. / Type-and-scope safe programs and their proofs. CPP 2017 : Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs. editor / Yves Bertot ; Viktor Vafeiadis. New York, 2017.
@inproceedings{eb48dd7561d5489a89dcdc1936a63537,
title = "Type-and-scope safe programs and their proofs",
abstract = "We abstract the common type-and-scope safe structure fromcomputations on lambda-terms that deliver, e.g., renaming, substitution, evaluation, CPS-transformation, and printing witha name supply. By exposing this structure, we can prove generic simulation and fusion lemmas relating operations built this way. This work has been fully formalised in Agda.",
keywords = "agda, dependently typed functional type , formal verification, lambda calculus, normalization by evaluation , syntax, semantics, mechanized meta theory, generic programming",
author = "Guillaume Allais and James Chapman and Conor McBride and James McKinna",
year = "2017",
month = "1",
day = "16",
doi = "10.1145/3018610.3018613",
language = "English",
isbn = "9781450347051",
editor = "Yves Bertot and Viktor Vafeiadis",
booktitle = "CPP 2017",

}

Allais, G, Chapman, J, McBride, C & McKinna, J 2017, Type-and-scope safe programs and their proofs. in Y Bertot & V Vafeiadis (eds), CPP 2017 : Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs. New York, 6th ACM SIGPLAN Conference on Certified Programs and Proofs, Paris, France, 16/01/17. https://doi.org/10.1145/3018610.3018613

Type-and-scope safe programs and their proofs. / Allais, Guillaume; Chapman, James; McBride, Conor; McKinna, James.

CPP 2017 : Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs. ed. / Yves Bertot; Viktor Vafeiadis. New York, 2017.

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

TY - GEN

T1 - Type-and-scope safe programs and their proofs

AU - Allais, Guillaume

AU - Chapman, James

AU - McBride, Conor

AU - McKinna, James

PY - 2017/1/16

Y1 - 2017/1/16

N2 - We abstract the common type-and-scope safe structure fromcomputations on lambda-terms that deliver, e.g., renaming, substitution, evaluation, CPS-transformation, and printing witha name supply. By exposing this structure, we can prove generic simulation and fusion lemmas relating operations built this way. This work has been fully formalised in Agda.

AB - We abstract the common type-and-scope safe structure fromcomputations on lambda-terms that deliver, e.g., renaming, substitution, evaluation, CPS-transformation, and printing witha name supply. By exposing this structure, we can prove generic simulation and fusion lemmas relating operations built this way. This work has been fully formalised in Agda.

KW - agda

KW - dependently typed functional type

KW - formal verification

KW - lambda calculus

KW - normalization by evaluation

KW - syntax

KW - semantics

KW - mechanized meta theory

KW - generic programming

UR - http://cpp2017.mpi-sws.org/index.html

UR - http://dl.acm.org/citation.cfm?id=3018610&CFID=889462538

U2 - 10.1145/3018610.3018613

DO - 10.1145/3018610.3018613

M3 - Conference contribution book

SN - 9781450347051

BT - CPP 2017

A2 - Bertot, Yves

A2 - Vafeiadis, Viktor

CY - New York

ER -

Allais G, Chapman J, McBride C, McKinna J. Type-and-scope safe programs and their proofs. In Bertot Y, Vafeiadis V, editors, CPP 2017 : Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs. New York. 2017 https://doi.org/10.1145/3018610.3018613