Zobrazeno 1 - 10
of 13
pro vyhledávání: '"Randy Pollack"'
Publikováno v:
Indagationes Mathematicae. 24:1073-1104
In this paper we introduce the notion of map, which is a notation for the set of occurrences of a symbol in a syntactic expression such as a formula or a λ term. We use binary trees over 0 and 1 as maps, but some well-formedness conditions are requi
Autor:
Roberto M. Amadio, Nicolas Ayache, Francois Bobot, Jaap P. Boender, Brian Campbell, Ilias Garnier, Antoine Madet, James McKinna, Randy Pollack, Yann Régis Gianas, Ian Stark, MULLIGAN, DOMINIC, PICCOLO, MAURO, SACERDOTI COEN, CLAUDIO, TRANQUILLI, PAOLO
We provide an overview of the FET-Open Project CerCo (‘Certified Complexity’). Our main achievement is the development of a technique for analysing non-functional properties of programs (time, space) at the source level with little or no loss of
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=od______4094::63ab0afdc952ebd282ae170746e6b686
http://hdl.handle.net/11585/386328
http://hdl.handle.net/11585/386328
Autor:
Masahiko Sato, Randy Pollack
Publikováno v:
Journal of Symbolic Computation. 45:598-616
It is well known that formally defining and reasoning about languages with binding (such as logics and λ-calculii) is problematic. There are many approaches to deal with the problem, with much work over recent years stimulated by the desire to forma
Autor:
Benjamin C. Pierce, Randy Pollack, André DeHon, Andrew Tolmach, Arthur Azevedo de Amorim, Nathan Collins, Delphine Demange, David Pichardie, Cătălin Hriţcu
Publikováno v:
POPL
Journal of Computer Security
Journal of Computer Security, 2016, 24 (6), pp.689--734. ⟨10.3233/JCS-15784⟩
41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)
41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2014, San Diego, CA, United States. ⟨10.1145/2535838.2535839⟩
Journal of Computer Security, IOS Press, 2016, 24 (6), pp.689--734. ⟨10.3233/JCS-15784⟩
Journal of Computer Security
Journal of Computer Security, 2016, 24 (6), pp.689--734. ⟨10.3233/JCS-15784⟩
41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)
41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2014, San Diego, CA, United States. ⟨10.1145/2535838.2535839⟩
Journal of Computer Security, IOS Press, 2016, 24 (6), pp.689--734. ⟨10.3233/JCS-15784⟩
International audience; SAFE is a clean-slate design for a highly secure computer system, with pervasive mechanisms for tracking and limiting information flows. At the lowest level, the SAFE hardware supports fine-grained programmable tags, with effi
Autor:
Roberto M. Amadio, François Bobot, Mauro Piccolo, Dominic P. Mulligan, James McKinna, Nicolas Ayache, Antoine Madet, Claudio Sacerdoti Coen, Brian Campbell, Ian Stark, Randy Pollack, Jaap Boender, Ilias Garnier, Yann Régis-Gianas, Paolo Tranquilli
Publikováno v:
Foundational and Practical Aspects of Resource Analysis ISBN: 9783319124650
FOPARA
FOPARA
We provide an overview of the FET-Open Project CerCo (‘Certified Complexity’). Our main achievement is the development of a technique for analysing non-functional properties of programs (time, space) at the source level with little or no loss of
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::deaf79badd1c6a1b7e3cfa6da846b087
https://doi.org/10.1007/978-3-319-12466-7_1
https://doi.org/10.1007/978-3-319-12466-7_1
Publikováno v:
CSF
The security literature offers a multitude of calculi, languages, and systems for information-flow control, each with some set of labels encoding security policies that can be attached to data and computations. The exact form of these labels varies w
This paper is about completely formal representation of languages with binding. We have previously written about a representation following an approach going back to Frege, based on first-order syntax using distinct syntactic classes for locally boun
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::92099619669a4e677353fddbaf9cd4f1
http://hdl.handle.net/11585/125776
http://hdl.handle.net/11585/125776
Autor:
Benoit Montagu, Ben Karel, Thomas F. Knight, Jonathan M. Smith, Robin Morisset, André DeHon, Greg Morrisett, Sumit Ray, Gregory Malecha, Randy Pollack, Benjamin C. Pierce, Olin Shivers, Gregory T. Sullivan
Publikováno v:
PLOS@SOSP
Safe is a clean-slate design for a secure host architecture. It integrates advances in programming languages, operating systems, and hardware and incorporates formal methods at every step. Though the project is still at an early stage, we have assemb
Autor:
Randy Pollack, John Longley
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783540230175
TPHOLs
TPHOLs
We consider the old problem of proving that a computer program meets some specification. By proving, we mean machine checked proof in some formal logic. The programming language we choose to work with is a call by value functional language, essential
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::d27b1a3c43e1c85e677c2759e513398d
https://doi.org/10.1007/978-3-540-30142-4_15
https://doi.org/10.1007/978-3-540-30142-4_15
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783540403326
TLCA
TLCA
Our long term goal is a system to formally represent complex structured mathematical objects, and proofs and computation on such objects; e.g. a foundational computer algebra system. Our approach is informed by the long development of module systems
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::703c2c2126c28b8eb76b26c5c69277e2
https://doi.org/10.1007/3-540-44904-3_8
https://doi.org/10.1007/3-540-44904-3_8