or cancel
  1. Dependently typed functional programming in Idris, 3 of 3

    59:14

    from Galois Video / Added

    115 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, 2 of 3

      01:02:47

      from Galois Video / Added

      146 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 by David Christiansen 1 of 3

        01:20:29

        from Galois Video / Added

        976 Plays / / 1 Comment

        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

          158 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

            30 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
            • Hacking Internet Voting via Ballot Tampering

              02:40

              from Galois Video / Added

              940 Plays / / 1 Comment

              Election Day was this week. If you took advantage of early voting, or you live overseas, you probably used a paper ballot you received in the mail a few weeks ago. A digital alternative, being considered…

              + More details
              • Tech talk by Philip Wadler

                01:19:31

                from Galois Video / Added

                74 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
                • Functional programming in Swift

                  48:59

                  from Galois Video / Added

                  133 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
                  • 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
                    • Verifying C programs in Coq using VST

                      57:05

                      from Galois Video / Added

                      24 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
                      • Verified Cryptographic Implementations

                        01:08:48

                        from Galois Video / Added

                        36 Plays / / 0 Comments

                        Abstract EasyCrypt is a computer-assisted framework for proving the security of cryptographic constructions. However, there is a significant gap between security proofs done in the usual provable…

                        + More details
                        • Vinyl: Records in Haskell and Type Theory

                          01:02:23

                          from Galois Video / Added

                          737 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

                          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