Constructor Functions

 

Title: Constructor Functions
Author: Lars Hupel
Submission date: 2017-04-19
Abstract: Isabelle's code generator performs various adaptations for target languages. Among others, constructor applications have to be fully saturated. That means that for constructor calls occuring as arguments to higher-order functions, synthetic lambdas have to be inserted. This entry provides tooling to avoid this construction altogether by introducing constructor functions.
BibTeX:
@article{Constructor_Funs-AFP,
  author  = {Lars Hupel},
  title   = {Constructor Functions},
  journal = {Archive of Formal Proofs},
  month   = apr,
  year    = 2017,
  note    = {\url{http://isa-afp.org/entries/Constructor_Funs.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License