Export to

• Google Calendar
• iCalendar file
• hCalendar markup
  <div class="vevent h-event"> <h1 class="summary p-name">Galois Tech Talk: Abstract "Anything": Theory and Proof Reuse via DTP</h1> <div class='date'><time class="dtstart dt-start" title="2012-08-28T10:30:00" datetime="2012-08-28T10:30:00">Tuesday, August 28, 2012 from 10:30</time>–<time class="dtend dt-end" title="2012-08-28T11:30:00" datetime="2012-08-28T11:30:00">11:30am</time></div> <div class="location vcard p-location h-card"> <a class="url" href='http://calagator.org/venues/202390439'><span class='fn org p-name'>Galois, Inc</span></a> <div class="adr p-adr h-adr"> <div class="street-address p-street-address">421 SW 6th Ave. Suite 300</div> <span class="locality p-locality">Portland</span> , <span class="region p-region">OR</span> <span class="postal-code p-postal-code">97204</span> <div class="country-name p-country-name">US</div> (<a href='https://maps.google.com/maps?q=421%20SW%206th%20Ave.%20Suite%20300,%20Portland%20OR%2097204%20US'>map</a>) </div> </div> <div class="description p-description"> <p>Presented by Larry Diehl.</p> <p>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.</p> <p>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.</p> </div> <h3>Links</h3> <ul> <li><a class="url u-url" href="http://corp.galois.com/blog/2012/8/21/tech-talk-abstract-anything-theory-and-proof-reuse-via-dtp.html">Website</a></li> </ul> </div>