Zobrazeno 1 - 10
of 815
pro vyhledávání: '"Olivier Danvy"'
Autor:
Olivier Danvy
Publikováno v:
ACM Transactions on Programming Languages and Systems. 45:1-35
In the tortoise-and-hare algorithm, when the fast pointer reaches the end of a finite list, the slow pointer points to the middle of this list. In the early 2000’s, this property was found to make it possible to program a palindrome detector for im
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::322751fe07429d0725d1176c7c3c5865
https://doi.org/10.1145/3564619
https://doi.org/10.1145/3564619
Autor:
OLIVIER DANVY
Publikováno v:
Journal of Functional Programming. 33
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::6588ca38a52e0e8905f6d22520a09adc
https://doi.org/10.1017/s0956796823000011
https://doi.org/10.1017/s0956796823000011
Autor:
OLIVIER DANVY
Publikováno v:
Journal of Functional Programming. 33
The equivalence of folding left and right over Peano numbers and lists makes it possible to minimalistically inter-derive (1) structurally recursive functions in direct style, (2) structurally tail-recursive functions that use an accumulator, and (3)
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b5ca98035ae1e2976741f06b633f2f35
https://doi.org/10.1017/s0956796822000156
https://doi.org/10.1017/s0956796822000156
Autor:
OLIVIER DANVY
Publikováno v:
Journal of Functional Programming. 32
Fold–unfold lemmas complement the rewrite tactic in the Coq Proof Assistant to reason about recursive functions, be they defined locally or globally. Each of the structural cases gives rise to a fold–unfold lemma that equates a call to this funct
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::05aefb97f6ed3d5fc0fe343e1815d0e4
https://doi.org/10.1017/s0956796822000107
https://doi.org/10.1017/s0956796822000107
Autor:
Luca Chiarabini, Olivier Danvy
Publikováno v:
Journal of Formalized Reasoning, Vol 4, Iss 1, Pp 85-109 (2011)
We revisit both the usual ``going-up'' induction principle and Manna and Waldinger's ``going-down'' induction principle for primitive recursion,`a la Goedel, and primitive iteration, `a la Church. We use 'Kleene's trick' to show that primitive recurs
Externí odkaz:
https://doaj.org/article/2728980411b74f01bedd86b74d224a04
Autor:
Olivier Danvy, Kevin Millikin
Publikováno v:
Logical Methods in Computer Science, Vol Volume 4, Issue 4 (2008)
Landin's SECD machine was the first abstract machine for applicative expressions, i.e., functional programs. Landin's J operator was the first control operator for functional languages, and was specified by an extension of the SECD machine. We presen
Externí odkaz:
https://doaj.org/article/ed42af3c80304a8e99b9c43060e2fc24
Publikováno v:
Logical Methods in Computer Science, Vol Volume 1, Issue 2 (2005)
We present an abstract machine and a reduction semantics for the lambda-calculus extended with control operators that give access to delimited continuations in the CPS hierarchy. The abstract machine is derived from an evaluator in continuation-passi
Externí odkaz:
https://doaj.org/article/6b6afdbdcae5419c8fef0c6d6517bf46
Autor:
Olivier Danvy
Publikováno v:
Journal of Functional Programming. 29
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::dfa5bcaa70eb68633e0fa0c34eb56f36
https://doi.org/10.1017/s0956796819000042
https://doi.org/10.1017/s0956796819000042
Autor:
Olivier Danvy
This essay accompanies a selection of 32 articles (referred to in bold face in the text and marginally marked in the bibliographic references) submitted to Aarhus University towards a Doctor Scientiarum degree in Computer Science. The author's previo
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::fcc23cfa669b5dcdcc33941f9c7567e5
https://doi.org/10.7146/aul.214.152
https://doi.org/10.7146/aul.214.152
Autor:
Peter Urbak, Olivier Danvy
Publikováno v:
A Formal Study of Moessner's Sieve
In this dissertation, we present a new characterization of Moessner's sieve that brings a range of new results with it. As such, we present a dual to Moessner's sieve that generates a sequence of so-called Moessner triangles, instead of a traditional
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::c12475dce34331077e969293eebf8eae
https://doi.org/10.7146/aul.213.154
https://doi.org/10.7146/aul.213.154