Monday, November 14, 2022, 3pm
Dependently-typed λ-calculi collapse the distinction between functional programs and proofs of their correctness, providing a theoretical foundation for verified sequential functional programming, raising the question: what of communicating processes? In this thesis proposal, we work towards a framework for unifying processes and proofs within an asynchronous process calculus via type refinements, which integrate verification conditions into type checking.
In prior work, we established that a limited form of dependent types enabled by arithmetic refinements allows mixed inductive-coinductive processes, which exhibit nested finite-infinite runtime behavior, to encode their own termination and productivity proofs. Then, we show that the corresponding type system is sound with respect to a model that we construct of terminating and productive process configurations via techniques from infinitary proof theory.
For the proposed work, we give preliminary evidence that full dependent types enabled by many-sorted logical refinements allow processes to prove Hoare-style specifications. In particular, we show that proofs of observational equalities between mixed inductive-coinductive processes, which certify runtime-behavioral equivalence, can themselves be such processes.
The ongoing work includes finalizing the generalized type system, extending our soundness result to it, and further metatheory.
Thesis Committee:
Frank Pfenning, Chair
Robert Harper
Karl Crary
Brigitte Pientka, McGill University
Additional Information
In Person and Zoom Participation. See announcement.
Event Type: Thesis Proposals
Room Number: In Person and Virtual - ET
Building: Gates Hillman 8102 and Zoom
Speaker's Name: SIVA KAMESH SOMAYYAJULA
Speaker Website: www.cs.cmu.edu…
Speaker's Professional Title: Ph.D. Student, Computer Science Department, Carnegie Mellon University
Talk Title: Type Refinements for Asynchronously Communicating Processes
Event Poster Title: Poster
Event Poster URL: www.cs.cmu.edu…
For More Information: deb@cs.cmu.edu
Affiliations: Computer Science Department (CSD)
Organization(s): SCS