14 ms·
Ask HN: What was the best CS paper you read in 2017?
- JelteF 9y agoThe raft consensus algorithm article [1] and the follow up that modifies it slightly with some changes that are useful when implementing it [2]. Both are written very clearly and very focused on actually using the algorithm in practice. Problems that arise when implementing it are discussed and solutions are proposed as well. [1] https://raft.github.io/raft.pdf https://raft.github.io/raft.pdf [2] http://openlife.cc/system/files/4-modifications-for-Raft-consensus.pdf http://openlife.cc/system/files/4-modifications-for-Raft-con...
- vjdhama 9y agoLifeguard : SWIM-ing with Situational Awareness https://arxiv.org/pdf/1707.00788.pdf https://arxiv.org/pdf/1707.00788.pdf
- nickpsecurity 9y agoI read a lot of good ones but I'll answer what was most important rather than best. We're seeing a revival of formal methods ranging from lightweight (TLA+) to heavy. Two problems are in my sight: lack of framework plus consistent, empirical data for evaluating how suitable a given method is for a specific project or company; many who would use lightweight or practical methods will quit because someone convinced them to start with heavy ones. The paper below is a start on the former: https://www.scch.at/de/rse-news/passende-formale-methon?file=files/Dokumente/SCCH_Web/Downloads/Downloads_2015/DownloadBilder/Neu_SCCH-TR-1603_FormalMethodsComparison.pdf https://www.scch.at/de/rse-news/passende-formale-methon?file... I think that was a great start on an evalution criteria because its comparisons match what I read in the various experience reports. ASM's and TLA+ coming in the lead on usability but B method on code generation. It will also help to note what projects have been completed or reusable libraries available in each. A person building verified compilers for functional languages might want to learn Isabelle/HOL due to CakeML, doing a new TLS extension learn F* due to miTLS, type-safe assembly learn Coq due to CoqASM, and so on. For the other issue, I made a proposal on HN first and then on Lobste.rs about avoiding people quitting early from finding formal methods too overwhelming or useless. I proposed having a default intro or lure that matched the goals of different people to tools with a warning of some's difficulty. It got some interesting responses (below) I'll turn into a mini-essay with links eventually. https://lobste.rs/s/n7v658/your_thoughts_on_this_advice_those https://lobste.rs/s/n7v658/your_thoughts_on_this_advice_thos...
- pron 9y agoTLA+ is by no means considered a lightweight formal method. It is proven relatively complete, i.e. anything that can be proven about a program, can be proven in TLA+. It can be used to only partially specify and verify a system, but so can Coq (usually, the term lightweight formal methods is applied to tools that can only specify/verify partially, or that that is their main intent). The main difference between TLA+ and other "deep" formal tools (Coq/Isabelle/Lean etc.) is that it is much easier to learn and apply. This is not because it is by any means lighter-weight in terms of software verification, but because of specific design choice which make it unsuitable to the primary goal of those other tools, namely formal proofs of "high" mathematics and the definition and exploration of novel logics. Those tools are so much harder to learn and use than TLA+ mainly because verifying programs is not their main goal. As a general math/logic proof assistant, TLA+ could certainly be considered lightweight, though :)
- nickpsecurity 9y agoMaybe I should've said TLA+ w/ model checking since that's definitely lightweight versus full, formal verification. Far as Lean, it's specifically designed for proving stuff about "complex systems."
- pron 9y ago> Maybe I should've said TLA+ w/ model checking since that's definitely lightweight versus full, formal verification. Why do you say that? Model checking is the most common form of full formal verification. It is true that because most TLA+ specifications -- unlike most software that's verified with model checkers -- has an infinite state space and that TLC, the model checker that's packaged with the TLA+ toolbox is an explicit state exploration model-checker with not support for infinite state spaces, then most of the time it is used on a finite-state derived specification and so doesn't fully verify the spec. But that is, AFAIK, not what is normally meant by "lightweight formal methods" (although I am not sure there is a very precise, well-accepted definition). But people take all sorts of short-cuts when working in Coq, too, and very rarely fully verify every aspect of the program. In fact, the only programs that were ever "fully" verified was 1. very small (much smaller than the vast majority of programs used in industry; I think jQuery is several times bigger than the biggest program ever "fully" verified end-to-end), 2. were heavily simplified in terms of algorithms used, and 3. took a loong time and required experts. So if that's how you'd classify "lightweight", then "full" doesn't exist in any meaningful sense. > Far as Lean, it's specifically designed for proving stuff about "complex systems." No, it's a Coq-style, general-purpose proof assistant. In any event, Coq, Lean and Isabelle are all designed for researchers. They are not aimed at industrial use at all. I know that the people behind Lean -- all accomplished experts in formal mathematics -- have made some claims about its suitability for verifying software, but AFAIK, none of them has any practical experience in software verification in industry, and so I find their claims to be entirely hypothetical. It's a beautiful proof assistant, but pragmatic software verification is not its first nor second goal. In contrast, TLA+ was designed with the help of actual "ordinary" industry engineers (at Compaq), who were using it for a large, real-world project, as it was being developed. That's the main difference between TLA+ and Coq/Lean -- it was designed as a product for engineers, not as a research tool for logicians.
- babangida 9y agoIt's an old one, but this year I read The Emperor's Old Clothes by C.A.R. Hoare for the first time and it got me started in a Hoare rabbit hole, just a brilliant guy. I read the annotated version on Fermat's Library - great source of interesting papers (http://fermatslibrary.com/s/the-emperors-old-clothes http://fermatslibrary.com/s/the-emperors-old-clothes).
- grajaganDev 9y ago* What Developers Want and Need from Program Analysis - An Empirical Study * Weird machines, exploitability, and provable unexploitability * What You Corrupt Is Not What You Crash: Challenges in Fuzzing Embedded Devices
- mafribe 9y ago* What Developers ...: http://ieeexplore.ieee.org/document/7582770 http://ieeexplore.ieee.org/document/7582770 (Sorry, no open version seems to be available) * Weird ...: http://ieeexplore.ieee.org/document/8226852 http://ieeexplore.ieee.org/document/8226852 * What You ...: http://s3.eurecom.fr/docs/ndss18_muench.pdf http://s3.eurecom.fr/docs/ndss18_muench.pdf
- spenrose 9y agoOpenly accessible "What Developers Want ..." https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/ase-2016.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/... obtained by pasting the title into scholar.google.com
- bra-ket 9y ago"Memcomputing NP-complete problems in polynomial time using polynomial resources and collective states" http://advances.sciencemag.org/content/1/6/e1500031.full http://advances.sciencemag.org/content/1/6/e1500031.full
- pelario 9y agoCould you tell us a bit about the reñevance of this work?
- DannyBee 9y agoThey claim they can actually build things that compute np-complete problems in polynomial time for real. "We show an experimental demonstration of an actual memcomputing architecture that solves the NP-complete version of the subset sum problem in only one step and is composed of a number of memprocessors that scales linearly with the size of the problem. We have fabricated this architecture using standard microelectronic technology so that it can be easily realized in any laboratory setting" This is traditionally what people look to quantum computing to solve, but that seems much farther off in practice that the technology described here, at least, as described. TL;DR Memcomputing has been shown to have the same power as non-deterministic turing machines. They claim to have made some real ones with promising results. It looks like it's getting commercialized over at http://memcpu.com/ http://memcpu.com/. I'm just summarizing the papers/data, not commenting on it for real, it could all just be snake oil
- godelmachine 9y agoThey have pretty much exaggerated their capability. I implore any curious HN reader to check out Scott Aaronson's review of their work & how he debunks it.
- chadcmulligan 9y agothanks, link for the impatient https://www.scottaaronson.com/blog/?p=2212 https://www.scottaaronson.com/blog/?p=2212
- indescions_2017 9y agoBringing The Web Up To Speed With WebAssembly https://github.com/WebAssembly/spec/blob/master/papers/pldi2017.pdf https://github.com/WebAssembly/spec/blob/master/papers/pldi2...
- trojanh 9y agoThat link seems to broken. Here the original link https://github.com/WebAssembly/spec/raw/master/papers/pldi2017.pdf https://github.com/WebAssembly/spec/raw/master/papers/pldi20... Definitely a good read.
- godelmachine 9y agoAdrian Colyer's review on WebAssembly was very helpful.
- sulam 9y agoI highly recommend people give this paper a read. I think it points the way to a radical redesign of fundamental parts of the system stack over the next 5-10 years. If you work in systems and you aren’t thinking about this stuff, you’re about to be lapped. The Case for Learned Index Structures: https://arxiv.org/pdf/1712.01208v1.pdf https://arxiv.org/pdf/1712.01208v1.pdf
- allcentury 9y agoThat was a good read, thanks for sharing this.
- AlexTelon 9y agoA very interesting read indeed! Besides HN how can one find great papers like this? How did you find out about it?
- CaHoop 9y agoI saw this paper on reddit.com/r/machinelearning - usually the more interesting ML papers are posted there. Additionally, there is http://www.arxiv-sanity.com/ http://www.arxiv-sanity.com/ which sorts new machine learning papers by popularity.
- sulam 9y agoI found this paper after reading through Jeff Dean's talk at NIPS. I recommend that, too, obviously! http://learningsys.org/nips17/assets/slides/dean-nips17.pdf http://learningsys.org/nips17/assets/slides/dean-nips17.pdf You can generally find a paper for each section.
- dekayed 9y agoI'd recommend taking a look at Papers We Love https://github.com/papers-we-love/papers-we-love https://github.com/papers-we-love/papers-we-love
- rmk 9y agoLoved the two-minute papers channel that I came across on this list. Thanks!
- icodemuch 9y agoThe bitcoin white paper (https://bitcoin.org/bitcoin.pdf https://bitcoin.org/bitcoin.pdf)
- saycheese 9y agoDoes anyone have any suggestions on finding CS papers worth reading beyond those papers listed here?
- azhenley 9y agoWhat topics are you interested in? Following the top ACM and IEEE conferences in that area is a good start! For example, I'm interested in human-computer interaction so I read CHI and UIST papers each year, and for software engineering I read ICSE and FSE.
- toomim 9y agoAh, if only CHI and UIST had good papers these days. :/
- azhenley 9y agoHey, I had a CHI paper this year! I think it publishes many great papers each year.
- toomim 9y agoWelcome to the echo chamber. In my experience, the only people who think CHI publishes great papers are the people publishing at CHI. (Disclosure: I've published at CHI a few times myself. I'm done with it.)
- vletrmx 9y agoSome Were Meant for C: The Endurance of an Unmanageable Language https://www.cl.cam.ac.uk/~srk31/research/papers/kell17some-preprint.pdf https://www.cl.cam.ac.uk/~srk31/research/papers/kell17some-p...
- azhenley 9y ago"Foraging Goes Mobile: Foraging While Debugging on Mobile Devices" (ftp://ftp.cs.orst.edu/pub/burnett/vlhcc17-foraging-mobile.pdf) "Toward Principles for the Design of Navigation Affordances in Code Editors: An Empirical Investigation" (http://dl.acm.org/authorize?N37917 http://dl.acm.org/authorize?N37917) "The Patchworks Code Editor: Toward Faster Navigation with Less Code Arranging and Fewer Navigation Mistakes" (http://dl.acm.org/authorize?N84177 http://dl.acm.org/authorize?N84177)
- kzrdude 9y agoThe most useful paper I read this year was Tidy Data (Wickham) http://vita.had.co.nz/papers/tidy-data.html http://vita.had.co.nz/papers/tidy-data.html
- CalChris 9y agoseL4: Formal Verification of an OS Kernel (from 2009). https://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf https://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf seL4 is about 9000 LOC. So this gives a good indication of what formal verification (Isabelle/HOL) is currently capable of. seL4 is also quite fast as a result of removing unnecessary checks. https://sel4.systems/ https://sel4.systems/ seL4 is smaller than L4Ka::Pistachio and it's also capability based which L4 isn't. They could have called it L5 or seL5.
- godelmachine 9y agoI want to learn formal verification on my own. Do you know of any resources? I got Rolf Dreshler's book on circuit verification, but I would like to master both hardware and software. Would you kindly provide with some pointers?
- CalChris 9y agoIt's a broad subject and I'm only interested in software verification. It's specialized enough that you should be reading papers and reading about systems. My favorite systems+papers are: Coq: The world’s best macro assembler? https://www.microsoft.com/en-us/research/publication/coq-worlds-best-macro-assembler/ https://www.microsoft.com/en-us/research/publication/coq-wor... Vale: Verifying High-Performance Cryptographic Assembly Code https://project-everest.github.io/assets/vale2017.pdf https://project-everest.github.io/assets/vale2017.pdf x86proved https://x86proved.codeplex.com/ https://x86proved.codeplex.com/
- mcguire 9y agoTwo schools: * Coq/dependent types. Check out Software Foundations by Benjamin Pierce, et. al. Everything's online. Also see Idris, which has a good book from Manning. * SMT-solver-based verification of existing languages. See SPARK/Ada (there's a good book but I can't remember the name presently) and the GNAT website. Also, Frama-C, although the documentation is more spotty. Then there's Rustan Leino's work on Dafny and Boogie. Oh, and Why3. And some work on verifying Java code that I haven't played with yet.
- anilshanbhag 9y agoChord: http://nms.lcs.mit.edu/papers/chord.pdf http://nms.lcs.mit.edu/papers/chord.pdf I think this paper amazing because it solves a complex problem with a simple solution. How do you create a hash function that adjust to the varying number of underlying buckets ? Solution: hash to a circle.
- nightcracker 9y agoIf you like Chord then you'll also like Kademlia.
- pedrosorio 9y agohttps://en.wikipedia.org/wiki/Consistent_hashing https://en.wikipedia.org/wiki/Consistent_hashing was actually introduced in 1997 by one of the authors of that paper.
- lwh 9y agoThis miserable blog post http://www.sicpers.info/2017/12/computings-fundamental-principle-of-no-learning/ http://www.sicpers.info/2017/12/computings-fundamental-princ...
- mcguire 9y agoT-t-t-taligent? My second real job out of college was with IBM's Taligent Project Office (where I independently invented mobile IP routing); I bailed as the wheels were coming if the IBM/Apple partnership.
- ky3 9y agoLeslie Lamport's 1978 "State the Problem Before Describing the Solution" [0]. On his web page the author adds that "The title says it all. This one-page note is as relevant today as when I wrote it. Replace "describing the solution" by "writing the program" and it becomes a practical recipe for improving software." Herewith, the paper in full: "After several years of writing papers in computer science, I discovered the basic expository rule embodied in the title of this note. As obvious as this rule may seem, there are fields in which it is seldom observed. (Computer networking is one example.) A typical paper in such a field is organized as follows: (1) a brief informal statement of the problem; (2) the solution; (3) a statement and proof of the precise correctness properties satisfied by the solution. In order to abide by the rule, the following organization should instead be used: (1) a brief informal statement of the problem; (2) the precise correctness conditions required of a solution; (3) the solution; (4) a proof that the solution satisfies the requisite conditions. Although it may not be obvious at first glance, there is a profound difference between these two approaches. In the first, the precise correctness conditions can be (and usually are) stated in terms of the solution itself. Some results are proved about the solution, but it is often not clear exactly what problem is being solved. This makes the comparison of two different solutions rather difficult. With the second approach, one is forced to specify the precise problem to be solved independently of the method used in the solution. This can be a surprisingly difficult and enlightening task. It has on several occasions led me to discover that a "correct" algorithm did not really accomplish what I wanted it to. I strongly urge everyone to observe the rule. (I am ignoring as unworthy of consideration the disturbingly large number of papers that never even attempt a precise statement of what problem they are solving.)" [0] https://lamport.azurewebsites.net/pubs/state-the-problem.pdf https://lamport.azurewebsites.net/pubs/state-the-problem.pdf
- tybit 9y agoThanks for this, this one is very relevant to industry(or at least to mine). The amount of software designs and programs that don't actually fit the technical/business problems from the get go is astounding.
- jonahx 9y ago> As obvious as this rule may seem, there are fields in which it is seldom observed. Indeed. Many -- perhaps even a majority of -- startup landing pages break this rule.
- akditer 9y agoWhat Makes A Great Software Engineer? https://faculty.washington.edu/ajko/papers/Li2015GreatEngineers.pdf https://faculty.washington.edu/ajko/papers/Li2015GreatEngine... Metaphors We Compute By Code is a story that explains how to solve a particular problem http://delivery.acm.org/10.1145/3130000/3127495/p40-videla.pdf?ip=178.24.248.117&id=3127495&acc=OPEN&key=4D4702B0C3E38B35%2E4D4702B0C3E38B35%2E4D4702B0C3E38B35%2E6D218144511F3437&CFID=1022155018&CFTOKEN=22940992&__acm__=1514658526_d143250fa6ef4ae196a6e0427d6e00dc http://delivery.acm.org/10.1145/3130000/3127495/p40-videla.p...
- johnsonjo 9y agoI found Knuth’s “Dancing Links” paper [1] very well written and a somewhat easy read (I had to reread certain parts a couple times). I had to write a sudoku solver for one of my classes and I read that dancing links and algorithm x was one way to do it [2]. I then read some things around the internet to apply dancing links to sudoku solving [3] [4]. If you read the Wikipedia entry on exact cover problems there is a section on sudoku as an exact cover problem [5] this is one thing necessary to understand in order to implement a sudoku solver with algorithm x and dancing links. Knuth even talks about dancing links in his new 2017 Christmas Tree Lecture [6] specifically here at 4:28 [7]. Basically he uses dancing links to solve for certain n in the problem he sets up in that lecture. [1] https://arxiv.org/abs/cs/0011047 https://arxiv.org/abs/cs/0011047 [2] https://en.wikipedia.org/wiki/Sudoku_solving_algorithms#Exact_cover https://en.wikipedia.org/wiki/Sudoku_solving_algorithms#Exac... [3] http://garethrees.org/2007/06/10/zendoku-generation/ http://garethrees.org/2007/06/10/zendoku-generation/ [4] https://www.ocf.berkeley.edu/~jchu/publicportal/sudoku/sudoku.paper.html https://www.ocf.berkeley.edu/~jchu/publicportal/sudoku/sudok... [5] https://en.wikipedia.org/wiki/Exact_cover#Sudoku https://en.wikipedia.org/wiki/Exact_cover#Sudoku [6] https://www.youtube.com/watch?v=BxQw4CdxLr8 https://www.youtube.com/watch?v=BxQw4CdxLr8 [7] https://youtu.be/BxQw4CdxLr8?t=4m28s https://youtu.be/BxQw4CdxLr8?t=4m28s
- svat 9y agoYou may like to know that Knuth's fascicle 5C of The Art of Computer Programming Volume 4 is going to be entirely about Dancing Links. He's still working on it, but the “incomplete draft” is available at the (hidden) link https://cs.stanford.edu/~knuth/fasc5c.ps.gz https://cs.stanford.edu/~knuth/fasc5c.ps.gz — check it out if you're interested; it's already 130 pages of fun.
- cynicaldevil 9y ago"Reflections on Trusting Trust": https://www.ece.cmu.edu/~ganger/712.fall02/papers/p761-thompson.pdf https://www.ece.cmu.edu/~ganger/712.fall02/papers/p761-thomp...
- AlexCoventry 9y agoEmergence of Invariance and Disentangling in Deep Representations https://arxiv.org/abs/1706.01350 https://arxiv.org/abs/1706.01350 "we show that in a deep neural network invariance to nuisance factors is equivalent to information minimality of the learned representation, and that stacking layers and injecting noise during training naturally bias the network towards learning invariant representations. We then show that, in order to avoid memorization, we need to limit the quantity of information stored in the weights, which leads to a novel usage of the Information Bottleneck Lagrangian on the weights as a learning criterion"
- beefman 9y agoProgramming languages Slepak et al - An Array-Oriented Language with Static Rank Polymorphism [1] Distributed systems Kiayias et al - A Provably Secure Proof-of-Stake Blockchain Protocol [2] Cognitive computing Boahen - A Neuromorph's Prospectus [3] Machine learning Silver et al - Mastering Chess and Shogi [4] 1 http://www.ccs.neu.edu/home/shivers/papers/rank-polymorphism.pdf http://www.ccs.neu.edu/home/shivers/papers/rank-polymorphism... 2 https://eprint.iacr.org/2016/889.pdf https://eprint.iacr.org/2016/889.pdf 3 https://pdfs.semanticscholar.org/3767/1e53c9949fa08d9dc150adf1ecaaca6f1880.pdf https://pdfs.semanticscholar.org/3767/1e53c9949fa08d9dc150ad... 4 https://arxiv.org/pdf/1712.01815.pdf https://arxiv.org/pdf/1712.01815.pdf
- posnet 9y agoA General-Purpose Counting Filter: Making Every Bit Count A better alternative to bloom filters and they provide a well written implementation as well https://github.com/splatlab/cqf https://github.com/splatlab/cqf https://www3.cs.stonybrook.edu/~ppandey/files/p775-pandey.pdf https://www3.cs.stonybrook.edu/~ppandey/files/p775-pandey.pd...
- NovaX 9y agoInterestingly this work has nearly identical algorithm to a previous paper. Good ideas are rediscovered. Counting with TinyTable: Every Bit Counts! http://www.cs.technion.ac.il/users/wwwb/cgi-bin/tr-get.cgi/2015/CS/CS-2015-04.pdf http://www.cs.technion.ac.il/users/wwwb/cgi-bin/tr-get.cgi/2...
- sktrdie 9y agoStatecharts: a visual formalism for complex systems: http://www.inf.ed.ac.uk/teaching/courses/seoc/2005_2006/resources/statecharts.pdf http://www.inf.ed.ac.uk/teaching/courses/seoc/2005_2006/reso... Even though it's from 1986 it's enlightening how useful it is to think about reactive systems using statecharts - especially as a UI developer this seems to make total sense and was a ah-ha moment when I first read it a couple months ago.
- wallflower 9y agoElegant and simple. Thank you for sharing it even though it is over 30 years old. Next time you happen to be at a store that has the rare, old fashioned-type automatic doors that swing out (not slide in/out), hurry out before your friends and stand on the pressure pad that is in the direction of the door swing out. No one will be able to exit. This is a simple example of a state machine in the real world that I like to use to explain more complex state machines.
- rozim 9y agoI probably enjoyed 'Mastering the game of Go with deep neural networks and tree search' the most and especially appreciated the 'Methods' section where they go into a good amount of detail about their implementation. https://storage.googleapis.com/deepmind-media/alphago/AlphaGoNaturePaper.pdf https://storage.googleapis.com/deepmind-media/alphago/AlphaG...
- superzamp 9y agoNot originally a CS paper, but this one describes a distributed algorithm medieval merchants used to simplify their debts graph: http://eh.net/eha/wp-content/uploads/2013/11/boerner.pdf http://eh.net/eha/wp-content/uploads/2013/11/boerner.pdf I highly recommend it to anyone interested in CS, history & finance.
- cygned 9y ago“The Evolution of LISP”, Steele/Gabriel (1993). PDF: https://www.csee.umbc.edu//courses/331/resources/papers/Evolution-of-Lisp.pdf https://www.csee.umbc.edu//courses/331/resources/papers/Evol... 80 pages, very well written and interesting.
- wk2jkhkjdfglsl 9y agoDullien, Thomas F. "Weird machines, exploitability, and provable unexploitability." IEEE Transactions on Emerging Topics in Computing (2017). http://ieeexplore.ieee.org/abstract/document/8226852/ http://ieeexplore.ieee.org/abstract/document/8226852/
- leecarraher 9y agoDynamic Routing Between Capsules the long awaited paper from Geoffrey Hinton (although Sara Sabour is principal author, Hinton has been hinting at this for a while now) on an alternative to back-propagation https://arxiv.org/abs/1710.09829 https://arxiv.org/abs/1710.09829
- tischler 9y agoHere are some experiments on more complext data and with more layers: https://arxiv.org/abs/1712.03480 https://arxiv.org/abs/1712.03480 Unfortunately, it does not look very promising so far.
- leecarraher 9y agowho down-votes a paper suggestion, and is too afraid to explain why.
- gnusouth 9y agoI really liked Vlad Zamfir's papers on "correct-by-construction" consensus protocols. What I love about this work is that it unifies traditional BFT consensus with blockchain consensus to make something better than both! Really exciting! Abstract CBC: https://github.com/ethereum/research/blob/master/papers/cbc-consensus/AbstractCBC.pdf https://github.com/ethereum/research/blob/master/papers/cbc-... Casper the friendly GHOST: https://github.com/ethereum/research/blob/master/papers/CasperTFG/CasperTFG.pdf https://github.com/ethereum/research/blob/master/papers/Casp... I found the Abstract CBC paper a little easier to understand, as it goes into more detail about the correct-by-construction process.
- alecco 9y agoA Seven-Dimensional Analysis of Hashing Methods and its Implications on Query Processing http://www.vldb.org/pvldb/vol9/p96-richter.pdf http://www.vldb.org/pvldb/vol9/p96-richter.pdf
- moretai 9y agoMay I ask why people read cs papers to gauge if I should be reading them?
- mbrodersen 9y agoI read CS papers to add more tools to my (mental) tool box.
- da-bacon 9y ago"Quantum advantage with shallow circuits" by Bravyi, Gosset, and Koenig https://arxiv.org/abs/1704.00690 https://arxiv.org/abs/1704.00690 What's beautiful about this paper is that it shows a provable separation in the power of quantum circuits over classical circuits. That is in contrast to many cases where quantum advantage is only suspected (the most notorious being Shor's algorithm: Factoring could be in P). Another cool thing is that this separation is fundamentally connected to quantum entanglement and the challenge of simulating measurements on multipartite quantum states with shared randomness and classical communication. This gives me some hope that this points to a path for future deep insights separating quantum from classical computing.
- jaseemabid 9y agoAn Incremental Approach to Compiler Construction[1] by Abdulaziz Ghuloum. The author presents a very approachable technique for building pedagogical compilers by starting with a tiny subset of the language - a language that can accept integers and print it and incrementally grows it into Scheme. Every step yields a fully working compiler for a progressively expanding subset of Scheme. Every compiler step produces real assembly code that can be assembled and executed directly by the hardware. I've dabbled with compilers for a while now and in my experience I found this to be among the best ways to get people excited about compilers. There is some code available from Nada Amin[2] for the curious and I'm re implementing it from scratch again[3]. 1. http://scheme2006.cs.uchicago.edu/11-ghuloum.pdf http://scheme2006.cs.uchicago.edu/11-ghuloum.pdf 2. https://github.com/namin/inc https://github.com/namin/inc 3. https://github.com/jaseemabid/inc https://github.com/jaseemabid/inc
- mhraza95 9y agohttp://www.thinkcode.xyz/benefits-using-angular-js/ http://www.thinkcode.xyz/benefits-using-angular-js/