or cancel
  1. Vinyl: Records in Haskell and Type Theory

    01:02:23

    from Galois Video / Added

    714 Plays / / 0 Comments

    abstract: Records in Haskell are notoriously difficult to compose; many solutions have been proposed. Vinyl lies in the space of library-level approaches, and addresses polymorphism, extensibility,…

    + More details
    • Sunroof and a Blank Canvas: A tail of two DSLs

      01:03:17

      from Galois Video / Added

      58 Plays / / 0 Comments

      Abstract Sunroof is an embedded Haskell Domain Specific Language (DSL) that compiles to JavaScript. Blank Canvas is an embedded Haskell DSL that provides direct access to the HTML5 JavaScript Canvas.…

      + More details
      • Haskell Bytes

        01:04:03

        from Galois Video / Added

        150 Plays / / 0 Comments

        abstract: We will take you on a guided tour through the memory of a running Haskell program and get to peek at the raw bytes of Haskell values. We’ll see how uniformity allows for polymorphic…

        + More details
        • Getting a Quick Fix on Comonads

          01:13:39

          from Galois Video / Added

          167 Plays / / 0 Comments

          abstract: While the monad abstraction has risen to a certain flavor of fame in the Haskell community and beyond, its equally fascinating dual, the comonad, remains relatively unknown. I’ll tell…

          + More details
          • Verifying C programs in Coq using VST

            57:05

            from Galois Video / Added

            23 Plays / / 0 Comments

            Abstract C programs are notoriously difficult to reason about, either for safety or full functional correctness. Even with a program logic powerful enough to prove the necessary properties, the proof…

            + More details
            • Automatic Device Driver Synthesis

              50:27

              from Galois Video / Added

              7 Plays / / 0 Comments

              abstract: Automatic device driver synthesis is a radical approach to creating drivers faster and with fewer defects by generating them automatically based on hardware device specifications. I will…

              + More details
              • Dependently typed functional programming in Idris, 2 of 3

                01:02:47

                from Galois Video / Added

                73 Plays / / 0 Comments

                abstract: Idris is a pure functional language with full dependent types. In this series of tech talks, Idris contributor David Christiansen will provide an introduction to programming in Idris as…

                + More details
                • Dependently typed functional programming in Idris, 3 of 3

                  59:14

                  from Galois Video / Added

                  48 Plays / / 0 Comments

                  abstract: Idris is a pure functional language with full dependent types. In this series of tech talks, Idris contributor David Christiansen will provide an introduction to programming in Idris as…

                  + More details
                  • Tech Talk: Common crypto mistakes in Android

                    48:44

                    from Galois Video / Added

                    123 Plays / / 0 Comments

                    abstract: If you do a web search for “encrypting Strings in Android”, you’ll find a lot of example code, and they all look pretty similar. They definitely input a String and output…

                    + More details
                    • Tech Talk: Read-copy update (RCU) validation and verification for Linux

                      01:07:11

                      from Galois Video / Added

                      17 Plays / / 0 Comments

                      abstract: Read-copy update (RCU) is a synchronization mechanism that is sometimes used as an alternative to reader-writer locking (among other things) that was added to the Linux kernel in 2002.…

                      + More details
                      • Functional programming in Swift

                        48:59

                        from Galois Video / Added

                        86 Plays / / 0 Comments

                        abstract: At this year’s WWDC, Apple announced Swift, a new programming language for iOS and OS X development. In this talk, I’d like to give a brief overview of the language, focussing…

                        + More details
                        • Tech talk by Philip Wadler

                          01:19:31

                          from Galois Video / Added

                          70 Plays / / 0 Comments

                          abstract: We present four calculi for gradual typing: λB, based on the blame calculus of Wadler and Findler (2009); λC, based on the coercion calculus of Henglein (1994); and λT…

                          + More details

                          Browse Videos

                          Galois Video

                          Here are all of the videos that Galois Video has uploaded to Vimeo. Appearances are videos that Galois Video has been credited in by others.

                          Also Check Out