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