Reading "Developing Verified Programs with Dafny" with Divyanshu Ranjan
Hosted on Zoom through the Hasgeek.com platform.
We will be reading Google's Spanner, by popular demand. Unmesh Joshi from ThoughtWorks will be presenting.
Venue: Online, through Hasgeek.com
We're going to discuss "The Tail at Scale" by Jeff Dean and Luiz André Barroso.
Piyush Goel will present the paper.
- Everyone comes to the meetup having read the paper
- The speaker will present the paper
- We will discuss the paper and ancillary topics
It's understood that not everyone will be able to read the paper beforehand, but we will not let that stop deeper discussions.
Software techniques that tolerate latency variability are vital to building responsive large-scale Web services.
Systems that respond to user actions quickly (within 100ms) feel more fluid and natural to users than those that take longer. Improvements in Internet connectivity and the rise of warehouse-scale computing systems have enabled web services that provide fluid responsiveness while consulting multi-terabyte datasets spanning thousands of servers; for example, the Google search system updates query results interactively as t…
Papers We Love, Bangalore chapter is back from its sabbatical!
We are starting with a paper very relevant to modern software architectures: "Your Server as a Function" by Marius Eriksen of Twitter.
This is a very accessible and readable paper, totalling 7 pages. Anyone who has designed and architected software systems or anyone who wants to do so will enjoy reading and discussing this paper.
You can download it from here: https://monkey.org/~marius/funsrv.pdf
Some of his other work can be found on the same website: https://monkey.org/~marius/
About the presenter:
Sherin from Protoship.io. He's a long time Rubyist and a Typed-FP practitioner in OCaml and ReasonML.
0. (Before the meetup) All of us read the paper and come
1. Sherin will present the paper
2. Themed discussions around the …
We will go through the AlphaGo paper (https://www.nature.com/articles/nature16961). In particular, I (Naren; https://nanonaren.com/) will focus on the generic Monte Carlo Tree Search algorithm; how it works; and, how it is specialized in this paper.
Remember that PWL is a discussion group, so please read the material beforehand as best as you can so we can have livelier discussions.
The location will be announced soon!
Thanks and see you there!…
This paper by Graham Hutton (http://www.cs.nott.ac.uk/~pszgmh/fold.pdf) provides a great introduction to reasoning with functional programs through the humble 'fold' operator. It gives an insight into how functional programs can be correct by construction and how functional programs can be programatically transformed. The audience is not expected to know functional programming... To help with understanding, I will express concretely many of the points covered in the paper in Haskell. Thanks!…
Available at: http://lamport.azurewebsites.net/pubs/time-clocks.pdf
As a summary, here is a quote from Leslie's website, about the paper (http://lamport.azurewebsites.net/pubs/pubs.html#time-clocks):
"...an algorithm for totally ordering events could be used to implement any distributed system. A distributed system can be described as a particular sequential state machine that is implemented with a network of processors. The ability to totally order the input requests leads immediately to an algorithm to implement an arbitrary state machine by a network of processors, and hence to implement any distributed system. So, I wrote this paper, which is about how to implement an arbitrary distributed state machine. As an illustration, I used the simplest example of a distributed system I could think of--…
• What we'll do
We will discuss the following paper: https://github.com/papers-we-love/papers-we-love/blob/master/distributed_systems/a-note-on-distributed-computing.pdf
We argue that objects that interact in a distributed system need to be dealt with in ways that are intrinsically different from objects that interact in a single address space. These differences are required because distributed systems require that the programmer be aware of latency, have a different model of memory access, and take into account issues of concurrency and partial failure.
We look at a number of distributed systems that have attempted to paper over the distinction between local and remote objects, and show that such systems fail to support basic requirements of robustness and reliability. These failures have been maske…
• What we'll do
1. A brief pitch for parsers, and their usage. We'll consider parsers outside of compilers, and programming language implementations i.e. parsers in everyday programming.
2. A dive into the approach suggested by the paper.
3. Implementation details, and comparing approaches in Haskell and Ruby. Chosen for their vastly different approach towards type systems and style of programming.
• What to bring
1. Your favourite note taking medium.
2. An open mind.
• Important to know
1. There won't be any hands-on exercises, or working through the paper.
Paper link: http://www.cs.nott.ac.uk/~pszgmh/parsing.pdf…
3D Computer Vision is the area of Computer Vision that studies how we can recreate 3D images of a 3D object, as opposed to normal cameras that create a 2D image of a 3D object. Application of this is abundant today: from Apple X's Augmented Reality applications, 3D Facial Recognition to latest news today Google Pixel use of Depth in images to create bokeh/Portrait images. Projective Geometry is the bread and butter of 3D Computer Vision. During this talk, we will see how Projective Geometry allows us to model the imaging process of a camera. Projective Geometry allows much more richer transformations than just translation and rotation possible in Euclidean Geometry. We will discuss how we can use Projective Geometry for various Computer Vision Problems: like Stereo, 3D Reconstruction etc.
It is a Joint session of Bangalore Co…
I find this paper by Abdulaziz Ghuloum extremely elegant and one of the most approachable introductions to compiler construction. I hope to present and demo a small compiler built in 24 incremental steps where each step is simple enough to grasp easily.
Full Title: Crowdsourcing Data Analysis: Do Soccer Referees Give More Red Cards to Dark Skin Toned Players?
Edit: Call Vipin at[masked] in case you have any difficulty in finding the venue.…
Manohar Jonnalagedda will talk about Scalable Component Abstractions
by Odersky and Zenger, published at OOPSLA 2005. He recently finished his PhD from Odersky's lab.
The paper that goes through 3 main features of the Scala language, and could arguably be considered as one of the base papers.
Let's discuss central limit theorem. . It's been an itch for me to understand that one, so I'll read up the background.…
We will be discussing the classic paper which kickstarted the area of Statistical Machine Translation.
The following is a explanatory document discussing the translation models, EM algorithm and provides mathematical proofs: http://www.cs.columbia.edu/~mcollins/courses/nlp2011/notes/ibm12.pdf
And finally, these are slides discussing the same material but with more examples and easier to understand: http://www.statmt.org/book/slides/04-word-based-models.pdf
Abstract: Eventual consistency aims to ensure that replicas of some mutable shared object converge without foreground synchronisation. Previous approaches to eventual consistency are ad-hoc and error-prone. We study a principled approach: to base the design of shared data types on some simple formal conditions that are sufficient to guarantee eventual consistency. We call these types Convergent or Commutative Replicated Data Types (CRDTs).
Overview: Replication is a fundamental concept of distributed systems. Any data update must be replicated to all peers in the system, if the system were to behave like a single system. This is usually achieved by introducing coordination, but it is expensive and can become infeasible quickly. An alternative approach is to build systems that are eventually co…
We have a meetup after a long break!
We are trying an alternate format for our talks and from now onward we will have multiple short talks instead of one long one. You can read more about the reasons to do so here.
Ramki will talk about Rsync.
Anand Pillai will talk about CAP theorem and here is the reading material.
1. This is the closest to "original paper" I could find. The idea was first proposed by Brewer in a talk.
Lessons from Giant-Scale Services,
Vaidhy will be presenting the famous FLP paper in distributed systems:
Fischer Lynch Paterson wrote a paper on Impossibility of Distributed Consensus with One Faulty Process :
Kashyap: Meetup.com's geolocation is kind of screwed up. Use this Gmaps link for directions on your mobile: https://goo.gl/maps/ikM7ekWGmUS2. The office is near the junction of Old Madras Road and IndiraNagar 100ft Road. Call [masked] for clarification. If you're heading towards old madras road on the 100ft Road, it's the last lane on the left side.…
I hope to present one of the earliest papers on Gradual Typing.
We will start with the basics.
• Various approaches of typing and the differences.
• Static, Gradual, Optional etc
• Contrast static and run time guarantees/behavior of untyped and typed lambda calculus
• Learn the Notation in Programming Language Theory
We will also look into other candidates in this space and what they do differently - like flowtype for js, typed racket, mypy etc.
Shriram is back at Bangalore and has agreed to give a talk on 17th Jan, Sunday evening.
Unlike other meetings, we *do not* have any reading material. Come with an open mind.
The Recurring Rainfall Problem
Soloway's Rainfall problem, a classic benchmark in computing education research, has proven difficult for many CS1 students. Rainfall tests students' abilities at plan composition, the task of integrating code fragments that implement subparts of a problem into a single program. Nearly all prior studies of Rainfall have involved students who were learning imperative programming with arrays. In our recent multi-university study, students learning functional programming produced atypical profiles of compositions and errors on Rainfall. What do these different results suggest about the problem of plan composition and programming education?
This talk raises various questions about the relationships between programming languages, progr…
Paper: By Peter M. Shor
Speaker: Anita SV.
Qubits, Phase estimation, Shor's Algorithm.
Link to Part 1
Paper: By Peter M. Shor
Speaker: Anita SV.
We will restrict this to just the introduction to Quantum Mechanics and Qubits.
Location: Ask for Cafeteria @ Inmobi office.
Link to Part 2:
Pre-requisites: Complex Numbers, Vectors, Trigonometry.
Good To Know: Fourier Transform, Number Theory.
Bonus: Linear Algebra, Hilbert Spaces, Quantum Mechanics.…
I plan to cover 2 papers. But the focus will definitely on the LSM-Tree paper.
As a brief intro will start with the B trees probably from (The ubiquitous B tree)
If people are intersted, I can show code for the some of the above.
Some knowledge of Database Internals and some basic algorithms is expected.
The reason this paper is important, is because most modern databases use either of the two ways for storing data.
I have started to create a Reading Helper for Reading the paper. It is here. If you are reading the paper and are confused about things please make a comment and I will update it.
Speaker: Anita SV (+ Vaidhy)…
I will be talking about Hyperloglog, a cardinality (i.e. number of distinct elements) estimation algorithm. In general, counting the number of elements in a set gets harder as the number of sets increase. For e.g., you might want to count number of users from a country.. i.e. number of sets is just 200+ and you can use a map of country to count. But, if you want to count the number of unique visitors to a popular website, then the number of sets become really large.
Probabilistic counting methods give a way to estimate the cardinality of sets without keeping track of every single item. Hyperloglog is probably the best known of those methods.
Prof. Shriram Krishnamurthi will be talking about his recent research on software defined networks and around the paper he co-authored "Tierless Programming and Reasoning for Software-Defined Networks". A link to the paper is here: http://cs.brown.edu/~adf/work/NSDI2014-paper.pdf
Some material to understand the paper better:
1. Introduction to the domain, helps to get a brief idea before diving into the paper. http://blog.brownplt.org/2014/09/30/flowlog1.html
Imperative programming is rooted in compulsively thinking of programs as a sequence of instructions given to a machine that manipulates a set of bits. Bits represent state: each bit can be in 2 states, 10 bits in 1024 states, a 100 in 1e301 states. No matter whatever high level abstractions you create for talking about these primitive bits (floats, points, lines, boxes, polygons, fish), as long as you are writing programs that work with state, you are bound to run into this combinatorial explosion as you add complexity. We humans are really bad at keeping track of states in our heads! An average person can keep
Vaidhy discussed Raft today (29th). He will followup on the Paxos paper by Leslie Lamport.…
Paxos and Raft are two algorithms for getting one answer from a group of unreliable processors. Some of the more popular use-cases for such algorithms are leader election, distributed locking, distributed log replication and so on.
Paxos was originally presented by Leslie Lamport in a very entertaining paper (that was rejected for publication many times). However, generalized Paxos is considered extremely hard to implement.
Raft was born as a easy to understand consensus algorithm and had several implementations to its credit.
In this session, I am planning to go over the problem of distributed log replication, walk through Paxos and its derivatives and then go through Raft. We can take a quick shot at implementing it, if time permits.…
Naren will be talking about the QuickCheck paper from John Hughes: http://www.cs.tufts.edu/~nr/cs257/archive/john-hughes/quick.pdf
slides and code:
Many of you have mentioned about this clashing with a talk at FuConf on property-based testing but I suggest we go through with this because I not only plan to cover QuickCheck but also motivate the topic with a little generality with respect to functional programming (to cater to those with a background mainly in imperative languages). Here is an outline of things I will cover
Each of these below will be illustrated with plenty of code examples
- Why are tests needed? This…
We will discuss and implement John McCarthy's 1978 paper "A Micro-manual for LISP -- not the whole truth".
Please read up the paper and work through it before coming into the meeting so that everyone benefits from the collective knowledge. The meetup will be very informal.…