Matches in UGent Biblio for { <https://biblio.ugent.be/publication/4132259#aggregation> ?p ?o. }
Showing items 1 to 29 of
29
with 100 items per page.
- aggregation classification "C1".
- aggregation creator person.
- aggregation creator person.
- aggregation date "2013".
- aggregation format "application/pdf".
- aggregation hasFormat 4132259.bibtex.
- aggregation hasFormat 4132259.csv.
- aggregation hasFormat 4132259.dc.
- aggregation hasFormat 4132259.didl.
- aggregation hasFormat 4132259.doc.
- aggregation hasFormat 4132259.json.
- aggregation hasFormat 4132259.mets.
- aggregation hasFormat 4132259.mods.
- aggregation hasFormat 4132259.rdf.
- aggregation hasFormat 4132259.ris.
- aggregation hasFormat 4132259.txt.
- aggregation hasFormat 4132259.xls.
- aggregation hasFormat 4132259.yaml.
- aggregation isPartOf urn:isbn:9781450323895.
- aggregation language "eng".
- aggregation publisher "Association for Computing Machinery (ACM)".
- aggregation rights "I have transferred the copyright for this publication to the publisher".
- aggregation subject "Science General".
- aggregation title "Generic datatypes a la carte".
- aggregation abstract "Formal reasoning in proof assistants, also known as mechanization, has high development costs. Building modular reusable components is a key issue in reducing these costs. A stumbling block for reuse is that inductive definitions and proofs are closed to extension. This is a manifestation of the expression problem that has been addressed by the Meta-Theory a la Carte (MTC) framework in the context of programming language meta-theory. However, MTC's use of extensible Church-encodings is unsatisfactory. This paper takes a better approach to the problem with datatype-generic programming (DGP). It applies well-known DGP techniques to represent modular datatypes, to build functions from functor algebras with folds and to compose proofs from proof algebras by means of induction. Moreover, for certain functionality and proofs our approach can achieve more reuse than MTC: instead of composing modular components we provide a single generic definition once and for all.".
- aggregation authorList BK318835.
- aggregation aggregates 4132260.
- aggregation isDescribedBy 4132259.
- aggregation similarTo LU-4132259.