Name
Abstract | ||
|---|---|---|
We focus on a common problem encountered in encoding and formally reasoning about a wide range of formal systems, namely, the representation of a typing environment. In particular, we apply the bookkeeping technique to a well-known case study (i.e., System F<:'s type language), proving in Coq an internal correspondence with a more standard representation of the typing environment as a list of pairs. In order to keep the signature readable and concise, we make use of higher-order abstract syntax (HOAS), which allows us to deal smoothly with the representation of the universal binder of System F<: type language. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1145/2631172.2631180 | LFMTP |
Keywords | Field | DocType |
specifying and verifying and reasoning about programs,logical frameworks,verification,higher-order abstract syntax,type theory,theory | Formal system,System F,Typing environment,Type theory,Theoretical computer science,Bookkeeping,Abstract syntax,Higher-order abstract syntax,Mathematics,Encoding (memory) | Conference |
Citations | PageRank | References |
1 | 0.35 | 18 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Alberto Ciaffaglione | 1 | 58 | 9.97 |
| Ivan Scagnetto | 2 | 232 | 20.87 |