Eugene Kirpichov. Ideas in type-theoretic theorem proving

Ligntning talk (~10')

Speaker: Jacek Migdal (Sumo Logic)

Title: Building Scala at scale

Description: How Sumo Logic achieves fast Scala compilation time through modularization and a few handy tricks

(from organizers)

This is a rather unusual topic for Scala meetups; but I think we need to refresh our brains and get some new ideas from outside the box (no pun)

Short description. This talk explains how writing programs and proving theorems are really the same thing, introducing one by one several of the most important ideas behind type-theoretic proof assistants such as Coq. No prior experience with type theory required.

Speaker's short bio. Eugene Kirpichov is an engineer at Google's distributed data processing frameworks team and a big fan of functional programming and related branches of mathematics.

Schedule

• 6:30-7:00 - networking

• 7:00-7:10 - announcements etc

• 7:10-~8:40 - talk

• 8:40-9:00 - networking