Matches in UGent Biblio for { <https://biblio.ugent.be/publication/3136387#aggregation> ?p ?o. }
Showing items 1 to 33 of
33
with 100 items per page.
- aggregation classification "C1".
- aggregation creator B89342.
- aggregation creator B89343.
- aggregation creator person.
- aggregation date "2013".
- aggregation format "application/pdf".
- aggregation hasFormat 3136387.bibtex.
- aggregation hasFormat 3136387.csv.
- aggregation hasFormat 3136387.dc.
- aggregation hasFormat 3136387.didl.
- aggregation hasFormat 3136387.doc.
- aggregation hasFormat 3136387.json.
- aggregation hasFormat 3136387.mets.
- aggregation hasFormat 3136387.mods.
- aggregation hasFormat 3136387.rdf.
- aggregation hasFormat 3136387.ris.
- aggregation hasFormat 3136387.txt.
- aggregation hasFormat 3136387.xls.
- aggregation hasFormat 3136387.yaml.
- aggregation isPartOf urn:isbn:9781450318327.
- 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 "Meta-theory à la carte".
- aggregation abstract "Formalizing meta-theory, or proofs about programming languages, in a proof assistant has many well-known benefits. Unfortunately, the considerable effort involved in mechanizing proofs has prevented it from becoming standard practice. This cost can be amortized by reusing as much of existing mechanized formalizations as possible when building a new language or extending an existing one. One important challenge in achieving reuse is that the inductive definitions and proofs used in these formalizations are closed to extension. This forces language designers to cut and paste existing definitions and proofs in an ad-hoc manner and to expend considerable effort to patch up the results. The key contribution of this paper is the development of an induction technique for extensible Church encodings using a novel reinterpretation of the universal property of folds. These encodings provide the foundation for a framework, formalized in Coq, which uses type classes to automate the composition of proofs from modular components. This framework enables a more structured approach to the reuse of meta-theory formalizations through the composition of modular inductive definitions and proofs. Several interesting language features, including binders and general recursion, illustrate the capabilities of our framework. We reuse these features to build fully mechanized definitions and proofs for a number of languages, including a version of mini-ML. Bounded induction enables proofs of properties for non-inductive semantic functions, and mediating type classes enable proof adaptation for more feature-rich languages.".
- aggregation authorList BK230624.
- aggregation endPage "217".
- aggregation startPage "208".
- aggregation aggregates 3136388.
- aggregation isDescribedBy 3136387.
- aggregation similarTo 2429069.2429094.
- aggregation similarTo LU-3136387.