Iowa Type Theory Commute artwork

Software Design and Intrinsic Identity

Iowa Type Theory Commute

English - January 21, 2021 04:00 - 9 minutes - 6.47 MB - ★★★★★ - 13 ratings
Technology Science Mathematics programming languages computational logic type theory proof assistants cedille Homepage Download Apple Podcasts Google Podcasts Overcast Castro Pocket Casts RSS feed
Previous Episode: Identity Inclusion in Relational Type Theory
Next Episode: Deriving disjointness of constructor ranges in RelTT

I muse about the hopeless prospect of a single intrinsic conceptual decomposition of a problem domain in software engineering, and relate this to the idea of intrinsic identity we discussed recently for Relational Type Theory.