Zobrazeno 1 - 10
of 12
pro vyhledávání: '"Neel Krishnaswami"'
Autor:
Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, Neel Krishnaswami
Despite significant progress in the verification of hypervisors, operating systems, and compilers, and in verification tooling, there exists a wide gap between the approaches used in verification projects and conventional development of systems softw
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::eeda41dd0949a14392dffee52c205013
Autor:
Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, Neel Krishnaswami
This repository contains the formalisation of the CN type system: definitions (defns.pdf) and the soundness proof of type checking (soundness.pdf). The formalisation is by Dhruv Makwana.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::9e8e63c2d43cf33a95161136e7cba0cd
Autor:
Faustyna Krawiec, Simon Peyton Jones, Neel Krishnaswami, Tom Ellis, Richard A. Eisenberg, Andrew Fitzgibbon
In this paper, we give a simple and efficient implementation of reverse-mode automatic differentiation, which both extends easily to higher-order functions, and has run time and memory consumption linear in the run time of the original program. In ad
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::5f386792e014b679436ccf420092a66a
https://www.repository.cam.ac.uk/handle/1810/334648
https://www.repository.cam.ac.uk/handle/1810/334648
Autor:
Christopher Pulte, Robert M. Norton, Ian Stark, Jon French, Alastair Reid, Shaked Flur, Alasdair Armstrong, Mark Wassell, Kathryn E. Gray, Peter Sewell, Neel Krishnaswami, Thomas Bauereiss, Brian Campbell, Prashanth Mundkur
Publikováno v:
Proceedings of the ACM on Programming Languages
Armstrong, A, Bauereiss, T, Campbell, B, Reid, A, Gray, K E, Norton, R M, Mundkur, P, Wassell, M, French, J, Pulte, C, Flur, S, Stark, I, Krishnaswami, N & Sewell, P 2019, ' ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS ', Proceedings of the ACM on Programming Languages, vol. 3, no. POPL, 71 . https://doi.org/10.1145/3290384
Armstrong, A, Bauereiss, T, Campbell, B, Reid, A, Gray, K E, Norton, R M, Mundkur, P, Wassell, M, French, J, Pulte, C, Flur, S, Stark, I, Krishnaswami, N & Sewell, P 2019, ' ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS ', Proceedings of the ACM on Programming Languages, vol. 3, no. POPL, 71 . https://doi.org/10.1145/3290384
Architecture specifications notionally define the fundamental interface between hardware and software: the envelope of allowed behaviour for processor implementations, and the basic assumptions for software development and verification. But in practi
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b03d45b0127eedfeee57ea420de43824
https://doi.org/10.1145/3290384
https://doi.org/10.1145/3290384
Publikováno v:
Proceedings of the ACM on Programming Languages
48th ACM SIGPLAN Symposium on Principles of Programming Languages
48th ACM SIGPLAN Symposium on Principles of Programming Languages
Step-indexed logical relations are an extremely useful technique for building operational-semantics-based models and program logics for realistic, richly-typed programming languages. They have proven to be indispensable for modeling features like hig
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::82f47a81ff5a0e151726f01b12921d5c
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783030719944
FoSSaCS
FoSSaCS
Most interaction with a computer is via graphical user interfaces. These are traditionally implemented imperatively, using shared mutable state and callbacks. This is efficient, but is also difficult to reason about and error prone. Functional Reacti
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a0c9d1c99f6f56239b5bcd4a7a1e9af4
https://doi.org/10.1007/978-3-030-71995-1_15
https://doi.org/10.1007/978-3-030-71995-1_15
Autor:
Neel Krishnaswami, Vikraman Choudhury
In this paper, we take a pervasively effectful (in the style of ML) typed lambda calculus, and show how to extend it to permit capturing pure expressions with types. Our key observation is that, just as the pure simply-typed lambda calculus can be ex
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::59edee0735f0a9a87eff3cbc61e4561c
Autor:
Neel Krishnaswami, Michael Arntzenius
© 2020 Copyright held by the owner/author(s). One of the workhorse techniques for implementing bottom-up Datalog engines is seminaïve evaluation. This optimization improves the performance of Datalog's most distinctive feature: recursively defined
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::ba5e3501e67f86e0fff2d3c56ea3bc2e
https://www.repository.cam.ac.uk/handle/1810/300767
https://www.repository.cam.ac.uk/handle/1810/300767
Publikováno v:
FARM@ICFP
Tonal music contains repeating or varying patterns that occur at various scales, exist at multiple locations, and embody diverse properties of musical notes. We define a language for representing music that expresses such patterns as musical transfor
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::8952cd47fb735305747a5d1c993498ff
https://doi.org/10.1145/3331543.3342586
https://doi.org/10.1145/3331543.3342586
Autor:
Jonathan Aldrich, Neel Krishnaswami
Publikováno v:
PLDI
Scopus-Elsevier
Scopus-Elsevier
Today's module systems do not effectively support information hiding in the presence of shared mutable objects, causing serious problems in the development and evolution of large software systems. Ownership types have been proposed as a solution to t
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8ad0836a0706a80f697671508701791c
https://doi.org/10.1145/1064978.1065023
https://doi.org/10.1145/1064978.1065023