Galois is pleased to host the following tech talk.
These talks are open to the interested public–please join us!
(There is no need to pre-register for the talk.)
title:
Abstract “Anything”: Theory and Proof Reuse via DTP
speaker:
Larry Diehl
time:
Tuesday, 28 August 2012, 10:30am
location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)
abstract:
Many advanced branches of mathematics involve
structures that abstract over well known specific instances, e.g. abstract
algebraic structures, equivalence relations, various orders, category theoretic
structures, etc. In typed functional programming (e.g. with type classes in
Haskell), encoding such structures amounts to enforcing the definition of
elements and operations for a particular structure instance on one hand, and
being able to use said elements and operations in generic definitions on the
other hand. With Dependently Typed Programming (DTP) we can go one step further
and define propositions/properties for abstract structures, and subsequently
require proofs in particular instances.
This talk will tell the story of how examples of particular instances inspire
an abstract definition (including its propositional properties), how to then
instantiate the original concrete examples in the new abstract definition, and
finally create further abstract definitions that depend on previously defined
ones. Emphasis will be given on how easily concrete proofs can be used as
evidence for abstract propositions, and how proofs about abstract structures
parameterized by other abstract structures may reuse their proofs (similar to
the more common concept of reusing operations in subsequent abstract
definitions). The talk will use Agda as its demonstration language, but proofs
will mostly be in the form of equational reasoning that should look familiar to
the non-expert.
bio: Larry Diehl is an incoming PhD student of Computer Science at
Portland State University. He has most recently worked for Engine Yard building
infrastructure for deploying web applications to cloud providers, and
previously got his bachelor’s degree from the University of Central Florida.
Larry has been merrily programming in Agda as a hobby for the last few years,
and some of his work can be seen on GitHub under the user larrytheliquid.