We provide a Lawvere-style definition for partial theories, extending the classical notion of equational theory by allowing partially defined operations. As in the classical case, our definition is syntactic: we use an appropriate class of string diagrams as terms. This allows for equational reasoning about the class of models defined by a partial theory. We demonstrate the expressivity of such equational theories by considering a number of examples, including partial combinatory algebras and cartesian closed categories. Moreover, despite the increase in expressivity of the syntax we retain a well-behaved notion of semantics: we show that our categories of models are precisely locally finitely presentable categories, and that free models exist.
Wed 20 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 17:00 | |||
16:00 10mTalk | A Computational Interpretation of Compact Closed Categories: Reversible Programming with Negative and Fractional Types POPL Link to publication DOI | ||
16:10 10mTalk | Internalizing Representation Independence with Univalence POPL Carlo Angiuli Carnegie Mellon University, Evan Cavallo Carnegie Mellon University, Anders Mörtberg Department of Mathematics, Stockholm University, Max Zeuner Stockholm University Link to publication DOI | ||
16:20 10mTalk | Petr4: Formal Foundations for P4 Data Planes POPL Ryan Doenges Cornell University, Mina Tahmasbi Arashloo Cornell University, Santiago Bautista Univ Rennes, ENS Rennes, Inria, IRISA, Alexander Chang Cornell University, Newton Ni Cornell University, Samwise Parkinson Cornell University, Rudy Peterson Cornell University, Alaia Solko-Breslin Cornell University, Amanda Xu Cornell University, Nate Foster Cornell University Link to publication DOI Pre-print | ||
16:30 10mTalk | The (In)Efficiency of Interaction POPL Beniamino Accattoli Inria & Ecole Polytechnique, Ugo Dal Lago University of Bologna, Italy / Inria, France, Gabriele Vanoni University of Bologna & INRIA Sophia Antipolis Link to publication DOI | ||
16:40 10mTalk | Functorial Semantics for Partial Theories POPL Chad Nester Tallinn University of Technology, Ivan Di Liberti Czech Academy of Sciences, Fosco Loregian Tallinn University of Technology, Pawel Sobocinski Tallinn University of Technology Link to publication DOI | ||
16:50 10mBreak | Break POPL |