[CS] [masters-presentation] Collins/MS Presentation/Nov 30, 2020

[Tricia Baclawski]

This is an announcement of Nicholas Collins's MS Presentation.


https://uchicago.zoom.us/j/95914628931?pwd=emoxbCtIRDd0M1oyT3ZpK3V4OUtzZz09
Password: 019707

------------------------------------------------------------------------------
Date:  Monday, November 30, 2020

Time:  10:00 AM

Place:  via zoom

M.S. Candidate:  Nicholas Collins

M.S. Paper Title: Delta Dictionaries: Total and Extensional Finite
Maps in Proof Assistants

Abstract:
Dictionaries, or finite maps, are a core data structure in any
programming language. General-purpose languages implement dictionaries
with hash tables or balanced trees, but proof assistants -- which
favor simplicity and provability over performance -- generally employ
association lists or finite partial functions. Though suitable for
many uses, each solution has drawbacks: association lists allow
arbitrary order and may contain duplicates (unless refined with an
explicit proof about validity), and partial functions cannot be
destructed and their equality is not decidable.

This paper illustrates a novel list-based representation, called delta
dictionaries, that simultaneously achieves benefits of the
conventional representations. Delta dictionaries are total (every
type-correct list is semantically valid), extensional (there is a
one-to-one correspondence between lists and semantic mappings),
destructible (sub-dictionaries can be inspected as needed), and have
decidable equality. Included is an implementation of delta
dictionaries and relevant metatheory in Agda, and a discussion of when
delta dictionaries may or may not be preferable to conventional
solutions.

Nicholas's advisor is Prof. Ravi Chugh

Login to the Computer Science Department website for details:
 https://newtraell.cs.uchicago.edu/phd/ms_announcements#nickmc

=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Tricia Baclawski
Student Affairs Administrator
Computer Science Department
5730 S. Ellis - Room 350
Chicago, IL 60637
pbaclawski at uchicago.edu
(773) 702-6854
/pronouns: she, her, hers/
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=