The OCaml Planet RSS

Smart contracts calls already provide a built-in authentication mechanism as transactions (i.e. call operations) are cryptographically signed by the sender of the transaction. This is a guarantee on which programs can rely. However, sometimes you may want more involved or flexible authentication sch...

Jane Street is sponsoring this year’s MakeMIThackathon, and we wanted to create a prize forthe winners that would do justice to the maker spirit of thecompet...

At Jane Street, over the last few years, we’ve been increasingly exploring machine learning to improve our models. Many of us are fascinated by the rapid imp...

Dmitrii Kovanikov's Personas Web Space

Presented by: Lindsey Kuper Parallel and distributed systems are notoriously difficult to build correctly or efficiently. In parallel systems, the manipulation of shared state can cause unintended behavior in the presence of unpredictable task scheduling, while in distributed systems, the manipulation of replicated state can cause unintended behavior in the presence of an unreliable network. Meanwhile, decades of research have not yet produced a general solution to the problem of automatic program parallelization. In this talk, I discuss how my research addresses these challenges from both theoretical and applied points of view. My work on lattice-based data structures, or LVars, proposes new foundations for expressive deterministic-by-construction parallel and distributed programming models. My work on non-invasive domain-specific languages for parallelism gives programmers language-based tools for safe, deterministic parallelization. The guiding principle and goal of both of these lines of work is to find the right high-level abstractions to express computation in a way that not only does not compromise efficiency, but actually enables it. I conclude by discussing the role that this principle of finding the right efficiency-enabling abstractions can play in my ongoing investigation into SMT-based verification of neural networks. Lindsey Kuper Lindsey Kuper (https://users.soe.ucsc.edu/~lkuper/) is an Assistant Professor of Computer Science and Engineering at the University of California, Santa Cruz, where she works on language-based approaches to building software systems that are correct and efficient. She holds a Ph.D. in computer science from Indiana University and a BA in computer science and music from Grinnell College. Prior to joining UC Santa Cruz, she was a Research Scientist in the Parallel Computing Lab at Intel Labs. During her Ph.D. years, she contributed to the Rust programming language at Mozilla Research, served several residencies at the Recurse Center, and co-founded !!Con (http://bangbangcon.com), the annual conference of ten-minute talks about the joy, excitement, and surprise of computing.

After the hard work done on the integration of floating-point arithmetic reasoning two years ago, 2018 is the year of polymorphic SMT2 support and efficient SAT solving for Alt-Ergo. In this post, we recap the main novelties last year, and we announce the first Alt-Ergo Users’ Club meeting. An SMT...

Generally, every program I write, regardless of what useful thing it actually does, and regardless of what programming language it is written in, has to do certain things, which usually includes Im…

MirageOS is a library operating system written from the ground up in OCaml. It has an impossible and incredibly huge goal to re-implement…