Type-and-scope safe programs and their proofs

Guillaume Allais; James Chapman; Conor McBride; James McKinna

doi:10.1145/3018610.3018613

Type-and-scope safe programs and their proofs

Guillaume Allais, James Chapman, Conor McBride, James McKinna

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

33 Citations (Scopus)

Abstract

We abstract the common type-and-scope safe structure from computations on terms that deliver, e.g., renaming, substitution, evaluation, CPS-transformation, and printing with a 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.

Original language	English
Title of host publication	CPP 2017: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs
Editors	Yves Bertot, Viktor Vafeiadis
Publisher	Association for Computing Machinery
Pages	195-207
Number of pages	13
ISBN (Electronic)	9781450347051
DOIs	https://doi.org/10.1145/3018610.3018613
Publication status	Published - 16 Jan 2017
Event	6th ACM SIGPLAN Conference on Certified Programs and Proofs 2017 - Paris, France Duration: 16 Jan 2017 → 17 Jan 2017

Conference

Conference	6th ACM SIGPLAN Conference on Certified Programs and Proofs 2017
Abbreviated title	CPP 2017
Country/Territory	France
City	Paris
Period	16/01/17 → 17/01/17

Keywords

Agda
Generic programming
Lambda-calculus
Mechanized meta-theory
Normalisation by evaluation
Semantics

ASJC Scopus subject areas

Software
Computer Science Applications

Access to Document

10.1145/3018610.3018613

Cite this

@inproceedings{434424c67e284822a7d8447bdb1efb3b,

title = "Type-and-scope safe programs and their proofs",

abstract = "We abstract the common type-and-scope safe structure from computations on terms that deliver, e.g., renaming, substitution, evaluation, CPS-transformation, and printing with a 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, Generic programming, Lambda-calculus, Mechanized meta-theory, Normalisation by evaluation, Semantics",

author = "Guillaume Allais and James Chapman and Conor McBride and James McKinna",

year = "2017",

month = jan,

day = "16",

doi = "10.1145/3018610.3018613",

language = "English",

pages = "195--207",

editor = "Yves Bertot and Viktor Vafeiadis",

booktitle = "CPP 2017: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs",

publisher = "Association for Computing Machinery",

address = "United States",

note = "6th ACM SIGPLAN Conference on Certified Programs and Proofs 2017, CPP 2017 ; Conference date: 16-01-2017 Through 17-01-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. Association for Computing Machinery, pp. 195-207, 6th ACM SIGPLAN Conference on Certified Programs and Proofs 2017, 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 et al.
CPP 2017: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs. ed. / Yves Bertot; Viktor Vafeiadis. Association for Computing Machinery, 2017. p. 195-207.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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 from computations on terms that deliver, e.g., renaming, substitution, evaluation, CPS-transformation, and printing with a 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 from computations on terms that deliver, e.g., renaming, substitution, evaluation, CPS-transformation, and printing with a 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 - Generic programming

KW - Lambda-calculus

KW - Mechanized meta-theory

KW - Normalisation by evaluation

KW - Semantics

UR - http://www.scopus.com/inward/record.url?scp=85015037327&partnerID=8YFLogxK

U2 - 10.1145/3018610.3018613

DO - 10.1145/3018610.3018613

M3 - Conference contribution

AN - SCOPUS:85015037327

SP - 195

EP - 207

BT - CPP 2017: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs

A2 - Bertot, Yves

A2 - Vafeiadis, Viktor

PB - Association for Computing Machinery

T2 - 6th ACM SIGPLAN Conference on Certified Programs and Proofs 2017

Y2 - 16 January 2017 through 17 January 2017

ER -

Type-and-scope safe programs and their proofs

Abstract

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this