A Mechanized Formalization of MicroKanren in Agda
Resumo
We present a machine-checked formalization of microKanren in the Agda proof assistant. Building on McBride’s accumulating most-general unifier, we develop a coinductive stream model for non-deterministic search with machine-verified soundness, completeness, and maximality for the unification goal. The stream type uses an inverted mutual record/data pair: a coinductive record KStream whose sole observation unfolds to an inductive Step with constructors fail, yield, and later. Corecursive definitions are written as copattern equations on .step; Agda’s guardedness checker accepts both fair interleaving and fair binding entirely without pragmas. The formalization is validated on two case studies: a logic puzzle and an infinite enumeration program. The entire development type-checks in the safe fragment of Agda 2.7.0.1 with the standard library 2.2.
Palavras-chave:
Agda, MicroKanren, Dependent Types, Coinduction, Unification
Referências
Andreas Abel, Brigitte Pientka, David Thibodeau, and Anton Setzer. 2013. Copatterns: Programming Infinite Structures by Observations. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’13). ACM, 27–38. DOI: 10.1145/2429069.2429075
Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, and James McKinna. 2021. A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs. Journal of Functional Programming 31 (2021), e22. DOI: 10.1017/S0956796820000076
Claire E. Alvis, Jeremiah J. Willcock, Kyle M. Carter, William E. Byrd, and Daniel P. Friedman. 2011. cKanren: miniKanren with Constraints. In Proceedings of the 2011 Workshop on Scheme and Functional Programming (Scheme ’11). [link]
William E. Byrd. 2009. Relational Programming in miniKanren: Techniques, Applications, and Implementations. Ph. D. Dissertation. Indiana University. [link]
Venanzio Capretta. 2005. General Recursion via Coinductive Types. Logical Methods in Computer Science 1, 2 (2005). DOI: 10.2168/LMCS-1(2:1)2005
Daniel P. Friedman, William E. Byrd, and Oleg Kiselyov. 2005. The Reasoned Schemer. The MIT Press. 176 pages.
Jason Hemann and Daniel P. Friedman. 2013. μKanren: A Minimal Functional Core for Relational Programming. In Proceedings of the 2013 Workshop on Scheme and Functional Programming (Scheme ’13).
Jason Hemann and Daniel P. Friedman. 2017. A Framework for Extending microKanren with Constraints. In Technical Communications of the 29th and 30th Workshops on (Constraint) Logic Programming and 24th International Workshop on Functional and (Constraint) Logic Programming (Electronic Proceedings in Theoretical Computer Science, Vol. 234). 135–149. DOI: 10.4204/EPTCS.234.10
Mathieu Jaume. 1999. A Full Formalization of SLD-Resolution in the Calculus of Inductive Constructions. Journal of Automated Reasoning 23, 3–4 (1999), 347–371. DOI: 10.1023/A:1006242018697
Pepijn Kokke and Wouter Swierstra. 2015. Auto in Agda: Programming Proof Search Using Reflection. In Mathematics of Program Construction — 12th International Conference, MPC 2015 (Lecture Notes in Computer Science, Vol. 9129). Springer, 205–227. DOI: 10.1007/978-3-319-19797-5_10
Per Martin-Löf. 1984. Intuitionistic Type Theory. Bibliopolis. Notes by Giovanni Sambin of a series of lectures given in Padova , June 1980.
Conor McBride. 2003. First-Order Unification by Structural Recursion. Journal of Functional Programming 13, 6 (2003), 1061–1075. DOI: 10.1017/S0956796803004957
Ulf Norell. 2007. Towards a Practical Programming Language Based on Dependent Type Theory. Ph. D. Dissertation. Chalmers University of Technology.
Ulf Norell. 2009. Dependently Typed Programming in Agda. In Advanced Functional Programming. Lecture Notes in Computer Science, Vol. 5832. Springer, 230–266. DOI: 10.1007/978-3-642-04652-0_5
Penny Press / Dell Magazines. 2016. Original Logic Problems. Penny Press / Dell Magazines, New York, NY. Recurring magazine; 128 pages, 90 logic problems per issue. [link].
Dmitry Rozplokhas, Andrey Vyatkin, and Dmitry Boulytchev. 2020. Certified Semantics for Relational Programming. In Programming Languages and Systems: 18th Asian Symposium, APLAS 2020, Fukuoka, Japan, November 30 – December 2, 2020, Proceedings (Fukuoka, Japan). Springer-Verlag, Berlin, Heidelberg, 167–185. DOI: 10.1007/978-3-030-64437-6_9
Philip Wadler, Wen Kokke, and Jeremy G. Siek. 2024. Programming Language Foundations in Agda. [link]
Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, and James McKinna. 2021. A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs. Journal of Functional Programming 31 (2021), e22. DOI: 10.1017/S0956796820000076
Claire E. Alvis, Jeremiah J. Willcock, Kyle M. Carter, William E. Byrd, and Daniel P. Friedman. 2011. cKanren: miniKanren with Constraints. In Proceedings of the 2011 Workshop on Scheme and Functional Programming (Scheme ’11). [link]
William E. Byrd. 2009. Relational Programming in miniKanren: Techniques, Applications, and Implementations. Ph. D. Dissertation. Indiana University. [link]
Venanzio Capretta. 2005. General Recursion via Coinductive Types. Logical Methods in Computer Science 1, 2 (2005). DOI: 10.2168/LMCS-1(2:1)2005
Daniel P. Friedman, William E. Byrd, and Oleg Kiselyov. 2005. The Reasoned Schemer. The MIT Press. 176 pages.
Jason Hemann and Daniel P. Friedman. 2013. μKanren: A Minimal Functional Core for Relational Programming. In Proceedings of the 2013 Workshop on Scheme and Functional Programming (Scheme ’13).
Jason Hemann and Daniel P. Friedman. 2017. A Framework for Extending microKanren with Constraints. In Technical Communications of the 29th and 30th Workshops on (Constraint) Logic Programming and 24th International Workshop on Functional and (Constraint) Logic Programming (Electronic Proceedings in Theoretical Computer Science, Vol. 234). 135–149. DOI: 10.4204/EPTCS.234.10
Mathieu Jaume. 1999. A Full Formalization of SLD-Resolution in the Calculus of Inductive Constructions. Journal of Automated Reasoning 23, 3–4 (1999), 347–371. DOI: 10.1023/A:1006242018697
Pepijn Kokke and Wouter Swierstra. 2015. Auto in Agda: Programming Proof Search Using Reflection. In Mathematics of Program Construction — 12th International Conference, MPC 2015 (Lecture Notes in Computer Science, Vol. 9129). Springer, 205–227. DOI: 10.1007/978-3-319-19797-5_10
Per Martin-Löf. 1984. Intuitionistic Type Theory. Bibliopolis. Notes by Giovanni Sambin of a series of lectures given in Padova , June 1980.
Conor McBride. 2003. First-Order Unification by Structural Recursion. Journal of Functional Programming 13, 6 (2003), 1061–1075. DOI: 10.1017/S0956796803004957
Ulf Norell. 2007. Towards a Practical Programming Language Based on Dependent Type Theory. Ph. D. Dissertation. Chalmers University of Technology.
Ulf Norell. 2009. Dependently Typed Programming in Agda. In Advanced Functional Programming. Lecture Notes in Computer Science, Vol. 5832. Springer, 230–266. DOI: 10.1007/978-3-642-04652-0_5
Penny Press / Dell Magazines. 2016. Original Logic Problems. Penny Press / Dell Magazines, New York, NY. Recurring magazine; 128 pages, 90 logic problems per issue. [link].
Dmitry Rozplokhas, Andrey Vyatkin, and Dmitry Boulytchev. 2020. Certified Semantics for Relational Programming. In Programming Languages and Systems: 18th Asian Symposium, APLAS 2020, Fukuoka, Japan, November 30 – December 2, 2020, Proceedings (Fukuoka, Japan). Springer-Verlag, Berlin, Heidelberg, 167–185. DOI: 10.1007/978-3-030-64437-6_9
Philip Wadler, Wen Kokke, and Jeremy G. Siek. 2024. Programming Language Foundations in Agda. [link]
Publicado
08/09/2026
Como Citar
HENKE, Eduardo; RIBEIRO, Rodrigo.
A Mechanized Formalization of MicroKanren in Agda. In: SIMPÓSIO BRASILEIRO DE LINGUAGENS DE PROGRAMAÇÃO (SBLP), 30. , 2026, São Paulo/SP.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2026
.
p. 54-62.
DOI: https://doi.org/10.5753/sblp.2026.27723.
