
TL;DR
This paper introduces a type system for Grassroots Logic Programs (GLP), enabling the formal typing of complex, multidirectional communication in concurrent logic programming, with implementation in Dart.
Contribution
It defines a new type system based on regular sets of moded paths, capturing communication directionality, and demonstrates its implementation and potential for AI-assisted programming.
Findings
Defined well-typing criteria for GLP programs.
Proved program correctness iff path semantics satisfy covariance and contravariance.
Implemented the type system in Dart with AI-generated specifications.
Abstract
Grassroots Logic Programs (GLP) is a concurrent logic programming language in which logic variables are partitioned into paired readers and writers. An assignment is produced at most once via a writer and consumed at most once via its paired reader, and may contain additional readers and/or writers. This enables the concise expression of rich multidirectional communication modalities. ``Logic Programs as Types for Logic Programs'' (LICS'91) defined types as regular sets of paths over derivable ground atoms. Here, we define types to be regular sets of moded paths, where a mode captures directionality of communication -- whether a subterm is consumed from or produced to the environment -- enabling the typing of interactive partial computations including those that eventually deadlock or fail, or never terminate. We provide a syntactic definition of well-typing and prove that a program…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
