BEGIN:VCALENDAR
PRODID;X-RICAL-TZSOURCE=TZINFO:-//Calagator//EN
CALSCALE:GREGORIAN
X-WR-CALNAME:Calagator
METHOD:PUBLISH
VERSION:2.0
BEGIN:VTIMEZONE
TZID;X-RICAL-TZSOURCE=TZINFO:America/Los_Angeles
BEGIN:DAYLIGHT
DTSTART:20120311T020000
RDATE:20120311T020000
TZOFFSETFROM:-0800
TZOFFSETTO:-0700
TZNAME:PDT
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20120821T181515Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20120828T113000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20120828T103000
DTSTAMP;VALUE=DATE-TIME:20120821T181515Z
LAST-MODIFIED;VALUE=DATE-TIME:20120821T181515Z
UID:http://calagator.org/events/1250462761
DESCRIPTION:Presented by Larry Diehl.
\;\n
\;\nMany advanced branch
es of mathematics involve structures that abstract over well known speci
fic instances\, e.g. abstract algebraic structures\, equivalence relatio
ns\, various orders\, category theoretic structures\, etc. In typed func
tional programming (e.g. with type classes in Haskell)\, encoding such s
tructures 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 subsequentl
y require proofs in particular instances.
\;\n
\;\nThis talk will
tell the story of how examples of particular instances inspire an abstra
ct definition (including its propositional properties)\, how to then ins
tantiate the original concrete examples in the new abstract definition\,
and finally create further abstract definitions that depend on previous
ly defined ones. Emphasis will be given on how easily concrete proofs ca
n be used as evidence for abstract propositions\, and how proofs about a
bstract structures parameterized by other abstract structures may reuse
their proofs (similar to the more common concept of reusing operations i
n subsequent abstract definitions). The talk will use Agda as its demons
tration language\, but proofs will mostly be in the form of equational r
easoning that should look familiar to the non-expert.\n\nTags: programmi
ng\, galois\, tech talk\, dependent types\n\nImported from: http://calag
ator.org/events/1250462761
URL:http://corp.galois.com/blog/2012/8/21/tech-talk-abstract-anything-the
ory-and-proof-reuse-via-dtp.html
SUMMARY:Galois Tech Talk: Abstract "Anything": Theory and Proof Reuse via
DTP
LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US
SEQUENCE:2
END:VEVENT
END:VCALENDAR