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 book

33 Citations (Scopus)

139 Downloads (Pure)

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.

Original language	English
Title of host publication	CPP 2017
Subtitle of host publication	Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs
Editors	Yves Bertot, Viktor Vafeiadis
Place of Publication	New York
Number of pages	13
DOIs	https://doi.org/10.1145/3018610.3018613
Publication status	Published - 16 Jan 2017
Event	6th ACM SIGPLAN Conference on Certified Programs and Proofs - Paris, France Duration: 16 Jan 2017 → 17 Jan 2017 Conference number: 6th http://cpp2017.mpi-sws.org/index.html

Conference

Conference	6th ACM SIGPLAN Conference on Certified Programs and Proofs
Abbreviated title	CPP 2017
Country/Territory	France
City	Paris
Period	16/01/17 → 17/01/17
Internet address	http://cpp2017.mpi-sws.org/index.html

Keywords

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

Access to Document

10.1145/3018610.3018613Licence: Unspecified

Allais-etal-CPP-2017-Type-and-scope-safe-programsAccepted author manuscript, 155 KB

Cite this

@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 = jan,

day = "16",

doi = "10.1145/3018610.3018613",

language = "English",

isbn = "9781450347051",

editor = "Yves Bertot and Viktor Vafeiadis",

booktitle = "CPP 2017",

note = "6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017 ; Conference date: 16-01-2017 Through 17-01-2017",

url = "http://cpp2017.mpi-sws.org/index.html",

}

TY - GEN

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

AU - Allais, Guillaume

AU - Chapman, James

AU - McBride, Conor

AU - McKinna, James

N1 - Conference code: 6th

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

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

Y2 - 16 January 2017 through 17 January 2017

ER -

Type-and-scope safe programs and their proofs

Abstract

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Conor McBride

Homotopy Type Theory: Programming and Verification