Zobrazeno 1 - 9
of 9
pro vyhledávání: '"Antal Spector-Zabusky"'
Autor:
JOACHIM BREITNER, ANTAL SPECTOR-ZABUSKY, YAO LI, CHRISTINE RIZKALLAH, JOHN WIEGLEY, JOSHUA COHEN, STEPHANIE WEIRICH
Publikováno v:
Journal of Functional Programming. 31
Good tools can bring mechanical verification to programs written in mainstream functional languages. We use hs-to-coq to translate significant portions of Haskell’s containers library into Coq, and verify it against specifications that we derive fr
Autor:
Stephanie Weirich, Yao Li, Christine Rizkallah, Antal Spector-Zabusky, John Wiegley, Joachim Breitner
Publikováno v:
Proceedings of the ACM on Programming Languages. 2:1-16
Good tools can bring mechanical verification to programs written in mainstream functional languages. We use hs-to-coq to translate significant portions of Haskell’s containers library into Coq, and verify it against specifications that we derive fr
Publikováno v:
CPP
We would like to use the Coq proof assistant to mechanically verify properties of Haskell programs. To that end, we present a tool, named hs-to-coq, that translates total Haskell programs into Coq programs via a shallow embedding. We apply our tool i
Autor:
Donald Spector, Antal Spector-Zabusky
Publikováno v:
Springer Proceedings in Mathematics & Statistics ISBN: 9783319911427
The graphical process of halftoning is, fundamentally, a communication process: an image made from a continuous set of possible grays, for example, is to be represented recognizably by elements that are only black or white. With this in mind, we ask
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::31939b74ad623d68abc79fd863a92dfc
https://doi.org/10.1007/978-3-319-91143-4_7
https://doi.org/10.1007/978-3-319-91143-4_7
Publikováno v:
Haskell
We present the urn, a simple tree-based data structure that supports sampling from and updating discrete probability distributions in logarithmic time. We avoid the usual complexity of traditional self-balancing binary search trees by not keeping val
Publikováno v:
TyDe@ICFP
We discuss a generalization of the synchronization mechanism selective choice. We argue that selective choice can be extended to synchronize arbitrary data structures of events, based on a typing paradigm introduced by McBride: the derivatives of rec
Autor:
Andrew Tolmach, Benjamin C. Pierce, Antal Spector-Zabusky, Arthur Azevedo de Amorim, Nick Giannarakis, Catalin Hritcu, Maxime Dénès
Publikováno v:
IEEE Symposium on Security and Privacy
2015 IEEE Symposium on Security and Privacy
2015 IEEE Symposium on Security and Privacy, May 2015, San Jose, United States. pp.813-830, ⟨10.1109/SP.2015.55⟩
2015 IEEE Symposium on Security and Privacy
2015 IEEE Symposium on Security and Privacy, May 2015, San Jose, United States. pp.813-830, ⟨10.1109/SP.2015.55⟩
International audience ; Recent advances in hardware design have demonstrated mechanisms allowing a wide range of low-level security policies (or micro-policies) to be expressed using rules on metadata tags. We propose a methodology for defining and
Autor:
Maxime Dénès, Dimitrios Vytiniotis, John Hughes, Antal Spector-Zabusky, Leonidas Lampropoulos, Arthur Azevedo de Amorim, Benjamin C. Pierce, Cătălin Hriţcu
Publikováno v:
Journal of Functional Programming
Journal of Functional Programming, Cambridge University Press (CUP), 2016, 26, e4 (62 p.). ⟨10.1017/S0956796816000058⟩
Journal of Functional Programming, 2016, 26, e4 (62 p.). ⟨10.1017/S0956796816000058⟩
Journal of Functional Programming, Cambridge University Press (CUP), 2016, 26, e4 (62 p.). ⟨10.1017/S0956796816000058⟩
Journal of Functional Programming, 2016, 26, e4 (62 p.). ⟨10.1017/S0956796816000058⟩
Information-flow control mechanisms are difficult both to design and to prove correct. To reduce the time wasted on doomed proof attempts due to broken definitions, we advocate modern random-testing techniques for finding counterexamples during the d
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::f9d413c675fd5414f05a7d47c0680d9a
http://arxiv.org/abs/1409.0393
http://arxiv.org/abs/1409.0393
Autor:
Leonidas Lampropoulos, Catalin Hritcu, Antal Spector-Zabusky, John Hughes, Arthur Azevedo de Amorim, Dimitrios Vytiniotis, Benjamin C. Pierce
Publikováno v:
ICFP
Information-flow control mechanisms are difficult to design and labor intensive to prove correct. To reduce the time wasted on proof attempts doomed to fail due to broken definitions, we advocate modern random testing techniques for finding counterex