Typed syntactic meta-programming

Dominique Devriese; Frank Piessens

doi:10.1145/2500365.2500575

Typed syntactic meta-programming

Dominique Devriese, Frank Piessens

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

8 Citations (Scopus)

Abstract

We present a novel set of meta-programming primitives for use in a dependently-typed functional language. The types of our meta-programs provide strong and precise guarantees about their termination, correctness and completeness. Our system supports typesafe construction and analysis of terms, types and typing contexts. Unlike alternative approaches, they are written in the same style as normal programs and use the language's standard functional computational model. We formalise the new meta-programming primitives, implement them as an extension of Agda, and provide evidence of usefulness by means of two compelling applications in the fields of datatype-generic programming and proof tactics.

Original language	English
Title of host publication	ICFP 2013 - Proceedings of the 2013 ACM SIGPLAN International Conference on Functional Programming
Publisher	Association for Computing Machinery, Inc
Pages	73-85
Number of pages	13
ISBN (Print)	9781450323260
DOIs	https://doi.org/10.1145/2500365.2500575
Publication status	Published - 12 Nov 2013
Event	2013 18th ACM SIGPLAN International Conference on Functional Programming, ICFP 2013 - Boston, MA, United States Duration: 25 Sep 2013 → 27 Sep 2013

Conference

Conference	2013 18th ACM SIGPLAN International Conference on Functional Programming, ICFP 2013
Country	United States
City	Boston, MA
Period	25/09/13 → 27/09/13

Keywords

Datatype-generic programming
Dependent types
Meta-programming
Tactics

Access to Document

10.1145/2500365.2500575

Link to publication in Scopus

Cite this

@inproceedings{0a5fdba0b5a3421a9d0da788caf03d40,

title = "Typed syntactic meta-programming",

abstract = "We present a novel set of meta-programming primitives for use in a dependently-typed functional language. The types of our meta-programs provide strong and precise guarantees about their termination, correctness and completeness. Our system supports typesafe construction and analysis of terms, types and typing contexts. Unlike alternative approaches, they are written in the same style as normal programs and use the language's standard functional computational model. We formalise the new meta-programming primitives, implement them as an extension of Agda, and provide evidence of usefulness by means of two compelling applications in the fields of datatype-generic programming and proof tactics.",

keywords = "Datatype-generic programming, Dependent types, Meta-programming, Tactics",

author = "Dominique Devriese and Frank Piessens",

year = "2013",

month = nov,

day = "12",

doi = "10.1145/2500365.2500575",

language = "English",

isbn = "9781450323260",

pages = "73--85",

booktitle = "ICFP 2013 - Proceedings of the 2013 ACM SIGPLAN International Conference on Functional Programming",

publisher = "Association for Computing Machinery, Inc",

note = "2013 18th ACM SIGPLAN International Conference on Functional Programming, ICFP 2013 ; Conference date: 25-09-2013 Through 27-09-2013",

}

Devriese, D & Piessens, F 2013, Typed syntactic meta-programming. in ICFP 2013 - Proceedings of the 2013 ACM SIGPLAN International Conference on Functional Programming. Association for Computing Machinery, Inc, pp. 73-85, 2013 18th ACM SIGPLAN International Conference on Functional Programming, ICFP 2013, Boston, MA, United States, 25/09/13. https://doi.org/10.1145/2500365.2500575

TY - GEN

T1 - Typed syntactic meta-programming

AU - Devriese, Dominique

AU - Piessens, Frank

PY - 2013/11/12

Y1 - 2013/11/12

N2 - We present a novel set of meta-programming primitives for use in a dependently-typed functional language. The types of our meta-programs provide strong and precise guarantees about their termination, correctness and completeness. Our system supports typesafe construction and analysis of terms, types and typing contexts. Unlike alternative approaches, they are written in the same style as normal programs and use the language's standard functional computational model. We formalise the new meta-programming primitives, implement them as an extension of Agda, and provide evidence of usefulness by means of two compelling applications in the fields of datatype-generic programming and proof tactics.

AB - We present a novel set of meta-programming primitives for use in a dependently-typed functional language. The types of our meta-programs provide strong and precise guarantees about their termination, correctness and completeness. Our system supports typesafe construction and analysis of terms, types and typing contexts. Unlike alternative approaches, they are written in the same style as normal programs and use the language's standard functional computational model. We formalise the new meta-programming primitives, implement them as an extension of Agda, and provide evidence of usefulness by means of two compelling applications in the fields of datatype-generic programming and proof tactics.

KW - Datatype-generic programming

KW - Dependent types

KW - Meta-programming

KW - Tactics

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

U2 - 10.1145/2500365.2500575

DO - 10.1145/2500365.2500575

M3 - Conference paper

AN - SCOPUS:84887186782

SN - 9781450323260

SP - 73

EP - 85

BT - ICFP 2013 - Proceedings of the 2013 ACM SIGPLAN International Conference on Functional Programming

PB - Association for Computing Machinery, Inc

T2 - 2013 18th ACM SIGPLAN International Conference on Functional Programming, ICFP 2013

Y2 - 25 September 2013 through 27 September 2013

ER -

Typed syntactic meta-programming

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this