Zobrazeno 1 - 10
of 55
pro vyhledávání: '"Morten Heine Sørensen"'
Autor:
Morten Heine Sørensen
Publikováno v:
Logical Methods in Computer Science, Vol Volume 3, Issue 4 (2007)
De Vrijer has presented a proof of the finite developments theorem which, in addition to showing that all developments are finite, gives an effective reduction strategy computing longest developments as well as a simple formula computing their length
Externí odkaz:
https://doaj.org/article/e8fcdf8cec894cc2a297fedda5a9660d
Autor:
Morten Heine Sørensen, Pawel Urzyczyn
The Curry-Howard isomorphism states an amazing correspondence between systems of formal logic as encountered in proof theory and computational calculi as found in type theory. For instance,minimal propositional logic corresponds to simply typed lambd
Autor:
Morten Heine Sørensen
Publikováno v:
Studia Logica. 107:1079-1081
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::6fc6c7f7e877f93f2dc4dc3a659ee007
https://doi.org/10.1007/s11225-019-09872-3
https://doi.org/10.1007/s11225-019-09872-3
Publikováno v:
VPT@CAV
A program transformation technique should terminate, return efficient output programs and be efficient itself.For positive supercompilation ensuring termination requires memoisation of expressions, and these are subsequently used to determine when to
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::0d5d46af935e265970943513ae0f4656
https://doi.org/10.29007/t4gz
https://doi.org/10.29007/t4gz
Autor:
Morten Heine Sørensen
Publikováno v:
Studia Logica. 101:1143-1145
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::40e5fe1ed92d33a2dbfbbc20db791254
https://doi.org/10.1007/s11225-013-9516-1
https://doi.org/10.1007/s11225-013-9516-1
Publikováno v:
Higher-Order and Symbolic Computation. 16:253-285
This paper offers a systematic account of techniques to infer strong normalization from weak normalization that make use of syntactic translations from λ-terms to λI-terms. We present variants of such techniques due to Klop, Sorensen, Xi, Gandy, an
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::9356b1ecac7dd91c4e0824e385d03745
https://doi.org/10.1023/a:1025693307470
https://doi.org/10.1023/a:1025693307470
Publikováno v:
Information and Computation. 178(1):149-179
For a notion of reduction in a λ-calculus one can ask whether a term satisfies conservation and uniform normalization. Conservation means that single-step reductions of the term preserve infinite reduction paths from the term. Uniform normalization
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::c135a2742d21044da210158bda52ce71
Publikováno v:
PEPM
Abramov and Glück have recently introduced a technique called URA for inverting first order functional programs. Given some desired output value, URA computes a potentially infinite sequence of substitutions/restrictions corresponding to the relevan
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::242cec6eef05d4015e76495d643abe3e
https://doi.org/10.1145/509799.503036
https://doi.org/10.1145/509799.503036
Publikováno v:
Theoretical Computer Science. 269(1-2):317-361
The Barendregt–Geuvers–Klop conjecture states that every weakly normalizing pure type system is also strongly normalizing. We show that this is true for a uniform class of systems which includes, e.g., the left-hand side of Barendregt's λ -cube
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a2762cec0f8f30a6f261f7830aeadde7
Publikováno v:
Theoretical Computer Science. 266:773-818
We present an induction principle for pure type systems and use that principle to define CPS translations and to solve the problem of expansion postponement for a large class of pure type systems. Our principle strengthens and generalises similar pri
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::ef1a10ec7d15b6a3e616871c007ed710
https://doi.org/10.1016/s0304-3975(00)00373-x
https://doi.org/10.1016/s0304-3975(00)00373-x