« Tech Talk: Formal Verification of Monad Transformers | Main | Galois Internship Available »

Tech Talk: Abstract "Anything": Theory and Proof Reuse via DTP

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

Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)


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.

Reader Comments

There are no comments for this journal entry. To create a new comment, use the form below.

PostPost a New Comment

Enter your information below to add a new comment.

My response is on my own website »
Author Email (optional):
Author URL (optional):
Some HTML allowed: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <code> <em> <i> <strike> <strong>