| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Code Generation for Functions as Data
| Title: | Code Generation for Functions as Data |
| Author: | Andreas Lochbihler |
| Submission date: | 2009-05-06 |
| Abstract: | FinFuns are total functions that are constant except for a finite set of points, i.e. a generalisation of finite maps. They are formalised as a new type in Isabelle/HOL such that the code generator can handle equality tests and quantification on FinFuns. On the code output level, FinFuns are explicitly represented by constant functions and pointwise updates, similarly to associative lists. Inside the logic, they behave like ordinary functions with extensionality. Via the update/constant pattern, a recursion combinator and an induction rule for FinFuns allow for defining and reasoning about operators on FinFun that are also executable. |
| Change history: | [2010-08-13]:
new concept domain of a FinFun as a FinFun
(revision 34b3517cbc09) [2010-11-04]: new conversion function from FinFun to list of elements in the domain (revision 0c167102e6ed) [2012-03-07]: replace sets as FinFuns by predicates as FinFuns because the set type constructor has been reintroduced (revision b7aa87989f3a) |
| BibTeX: |
@article{FinFun-AFP,
author = {Andreas Lochbihler},
title = {Code Generation for Functions as Data},
journal = {Archive of Formal Proofs},
month = may,
year = 2009,
note = {\url{http://isa-afp.org/entries/FinFun.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Used by: | Extended_Finite_State_Machines, JinjaThreads, Launchbury, Nominal2 |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |