Zobrazeno 1 - 10
of 50
pro vyhledávání: '"Harry G. Mairson"'
Autor:
Harry G. Mairson
Publikováno v:
ICFP
We describe a functional programming approach to the design of outlines of eighteenth-century string instruments. The approach is based on the research described in François Denis's book, Traité de lutherie . The programming vernacular for Denis's
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::66d65ee67b1640f52f17a3fef13f99b4
https://doi.org/10.1145/2544174.2500617
https://doi.org/10.1145/2544174.2500617
Autor:
Harry G. Mairson
Publikováno v:
Journal of Functional Programming. 14:623-633
We give transparent proofs of the PTIME-completeness of two decision problems for terms in the λ-calculus. The first is a reproof of the theorem that type inference for the simply-typed λ-calculus is PTIME-complete. Our proof is interesting because
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a72b1347dedb81448e3c4a709b2c9e9d
https://doi.org/10.1017/s0956796804005131
https://doi.org/10.1017/s0956796804005131
Publikováno v:
ICFP
Useful type inference must be faster than normalization. Otherwise, you could check safety conditions by running the program. We analyze the relationship between bounds on normalization and type inference. We show how the success of type inference is
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::53c540d3eca7018580b6009d25c2cbfe
https://doi.org/10.1145/1016848.1016871
https://doi.org/10.1145/1016848.1016871
Publikováno v:
ACM SIGPLAN Notices. 34:90-101
We investigate finite-rank intersection type systems, analyzing the complexity of their type inference problems and their relation to the problem of recognizing semantically equivalent terms. Intersection types allow something of type τ 1 Λ τ 2 to
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::10bd3fd380b2200fe778b98ba993b4e2
https://doi.org/10.1145/317765.317788
https://doi.org/10.1145/317765.317788
Autor:
Harry G. Mairson, Fritz Henglein
Publikováno v:
Journal of Functional Programming. 4:435-477
We analyse the computational complexity of type inference for untyped λ-terms in the second-order polymorphic typed λ-calculus (F2) invented by Girard and Reynolds, as well as higher-order extensionsF3,F4, …,Fωproposed by Girard. We prove that r
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::555acdb60575568bd2b72267fa031853
https://doi.org/10.1017/s0956796800001143
https://doi.org/10.1017/s0956796800001143
Autor:
Harry G. Mairson
Publikováno v:
Information Processing Letters. 49:95-99
Given an unambiguous context-free grammar G and an integer n > 0, we give two algorithms for generating words derived from the grammar uniformly at random (u.a.r.). The first algorithm generates a word u.a.r. in O( n 2 ) time using a data structure o
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::3ad27f392084adbc82e90d47c43b8357
https://doi.org/10.1016/0020-0190(94)90033-7
https://doi.org/10.1016/0020-0190(94)90033-7
Publikováno v:
Journal of the ACM. 40:683-713
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::f842e420a1aa0711c3348f21a783545b
https://doi.org/10.1145/174130.174142
https://doi.org/10.1145/174130.174142
Autor:
Harry G. Mairson
Publikováno v:
Theoretical Computer Science. 103:387-394
In this note, we reprove a theorem of Statman that deciding the βη-equality of two first-order typable λ-terms is not elementary recursive (Statman, 1982). The basic idea of our proof, like that of Statman's is the Henkin quantifier elimination pr
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::cae2a5c06ddd16fa67650a67c4092962
https://doi.org/10.1016/0304-3975(92)90020-g
https://doi.org/10.1016/0304-3975(92)90020-g
Autor:
Harry G. Mairson
Publikováno v:
BIT. 32:430-440
It has been shown by various researchers that designing a perfect hashing function for a fixed set ofn elements requires Θ(n) bits in the worst case. A possible relaxation of this scheme is to partition the set into pages, and design a hash function
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::1f77282cfba9f83feebe7653cd493e9d
https://doi.org/10.1007/bf02074879
https://doi.org/10.1007/bf02074879
Autor:
Harry G. Mairson
Publikováno v:
Journal of Functional Programming. 2:213-226
We present a simple and easy-to-understand explanation of ML type inference and parametric polymorphism within the framework of type monomorphism, as in the first order typed lambda calculus. We prove the equivalence of this system with the standard
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::8357a2957e43800ceac18d271fb3518b
https://doi.org/10.1017/s0956796800000332
https://doi.org/10.1017/s0956796800000332