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

    01:02:47

    from Galois Video / Added

    161 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
    • Model-based Code Generation and Debugging of Concurrent Programs

      01:02:29

      from Galois Video / Added

      108 Plays / / 0 Comments

      abstract: Design and implementation of distributed systems often involve many subtleties due to their complex structure, non-determinism, and low atomicity as well as occurrence of unanticipated physical…

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

        01:02:23

        from Galois Video / Added

        739 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
        • Computers As We Don’t Know Them

          01:02:00

          from Galois Video / Added

          1,712 Plays / / 0 Comments

          For slides and more details, please visit: http://www.galois.com/blog/2010/08/11/tech-talk-computers-as-we-dont-know-them/

          + More details
          • New Directions in Random Testing - From Mars Rovers to JavaScript Engines

            01:01:02

            from Galois Video / Added

            75 Plays / / 0 Comments

            abstract: One of the most effective ways to test complex language implementations, file systems, and other critical systems software is random test generation. This talk will cover a number of recent…

            + More details
            • Large-Scale Static Analysis at Mozilla

              01:00:40

              from Galois Video / Added

              2,249 Plays / / 1 Comment

              Mozilla Firefox is one of the largest open source C++ projects. Unfortunately C++ is a complex language: method overloading, virtual functions, template instantiation, pointer arithmetic, etc reduce…

              + More details
              • Formal Verification of Cyber-Physical Systems

                59:34

                from Galois Video / Added

                103 Plays / / 0 Comments

                abstract: Cyber-Physical Systems (CPS) refer to systems in which control, computation and communication converge to achieve complex functionalities. The ubiquitous deployment of cyber-physical systems…

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

                  59:14

                  from Galois Video / Added

                  116 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
                  • Programming Diversity

                    58:09

                    from Galois Video / Added

                    151 Plays / / 0 Comments

                    abstract: It's been scientifically proven that more diverse communities and workplaces create better products and the solutions to difficult problems are more complete and diverse themselves.…

                    + More details
                    • The SMACCMPilot Project: New Techniques for Embedded Programming

                      57:45

                      from Galois Video / Added

                      72 Plays / / 0 Comments

                      abstract: At Galois, we're building critical flight control software using new software methods for embedded systems programming. We will show how we used new domain-specific languages which…

                      + 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
                        • Verifying seL4-Based Systems

                          55:53

                          from Galois Video / Added

                          282 Plays / / 0 Comments

                          abstract: In 2009 the NICTA L4.verified project completed the machine-checked correctness proof of the seL4 microkernel. The natural next step is then to use this verified kernel to construct verified…

                          + 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