Modules

Racket modules. Wassup with those? Supposedly racket has a very sophisitcated module system

(module Foo (T) 
()
()
()
)

racket modules https://docs.racket-lang.org/guide/module-basics.html ocaml modules

Modules.

They are interesting. I get the impression from the leroy paper that modules are not persay tied to language https://ocaml.org/docs/papers.html

Higher Order Mdules and the Phase Distinction phase distinction What are recursive modules?

modular modules Really great paper

Modular Verification Scopes via Export Sets and Translucent Exports K. Rustan M. Leino and Daniel Matichuk

Can I use a module system a la ocaml for pure assembly programs?

Can one build a module system that is language agnostic as some kind of preprocessing tool?

Goguen paper obj https://cseweb.ucsd.edu/~goguen/pps/utyop.pdf “parametrized programming”

From whence did modules come?

https://grosskurth.ca/bib/1997/cardelli.pdf - Program Fragments, Linking, and Modularization Luca Cardelli

Hmm We could ust pick the simplest language possible Cardelli uses simply typed lambda. I guess that makes sense

algerbaic specification - Algebraic specification : syntax, semantics, structure https://escholarship.org/content/qt46b0f4z3/qt46b0f4z3.pdf?t=q6958g Woah there is a whole world here Obj, Clear, CASL, CIP, ASL others. What the hell happened to this https://en.wikipedia.org/wiki/Common_Algebraic_Specification_Language Goguen burstall wirsing ehrig http://maude.cs.illinois.edu/w/index.php/Maude_Overview descendent of obj3 http://maude.cs.illinois.edu/w/images/6/65/Maude-3.2.1-manual.pdf chapter 6 is interesintg protecting,extending, inlcuding. Modules represent their initial models. Huh.

I wonder what prolog has to say about modules. Well, lambda prolog has modules. I know that

different underlying logic. Conditional equational is one

ocaml doesn’t let you write equations in the module interface https://www.cs.cornell.edu/courses/cs3110/2021sp/textbook/fm/alg_spec.html

Make egglog have modules and signatures.

pushout constructions for modules. Could I literally use the ocaml module system and maintain equations at the value level using egraphs?

Interesting examples for egglog https://www.cs.scranton.edu/~mccloske/courses/se507/alg_specs_lec.html stacks, queues, etc.

intro to algerbaic specification part 1 https://watermark.silverchair.com/35-5-460.pdf?token=AQECAHi208BE49Ooan9kkhW_Ercy7Dm3ZL_9Cf3qfKAc485ysgAAAswwggLIBgkqhkiG9w0BBwagggK5MIICtQIBADCCAq4GCSqGSIb3DQEHATAeBglghkgBZQMEAS4wEQQM4uuASII9TSk95r9ZAgEQgIICfzXjI97KYQjpc_SnuFCooso2W1PN5dBZSijCJ-WygpqFTuaM8UgHT_we6cUpVHZrae9EKQjX4noQjoVrNkt37oYJi7Yu4RsyfUb3X0wmrb1SgdoFTTyeze34r1sHYk2s9fZbhk4TgfhsH56hDBvMd2I8qHeJ4D9HzFZouO7RNLDnAqldLQBR5esSDbs34tD0y74fi7UVJ6ynQlQDyT8KR73itnGvS5ZaqamJRI6S1A__ozhileTejT-4gE79uWqITyzrymHRmDsfIF2XvTaIimCwrUOHMlXJQ4IlGUEx2qA9ZO7Z0KK0LmveUF8ycbuaxGpkDiRoG3PBaiCG7LWNnJuRzg9Dzp_WaYOjvAZ4DsWzBTORZYJVnJWZLNXl-Irq0_u24V-qqHNQfZd8OhjILEeq6unqUXAJpRPKfkFr9oAd02PZXhLdw5KiI4YRwcUYEY6SzBmaNBA6z_TuvNHRueiocAiBZy8CzVBnRMx_HGWSoF-UHG9bTUoDynOM1iEU6bUUmN3IZmhlpY8LLVPYFNg_7i_8vffKzpGdW_nztlTHxTEFSpytzkAmYN8TYQV-o1KWksd22kFgsGCZIY0ZBmdM7liDHs2xS4kkuccBlxwX9OKpKVjy39HZ9p-3A3WSxJYzr1eOGjQn1zr3niIyRam42dS2Nwnxz442Hs7mBFNNqMusD1bUTHfUTBq4t-VhQ4a6oJHsepIj4Cdu5dLw2KYAlAc1rpWHbVXhGvIQqjvjo-XX625hgQzYuOXdjENJ2-f51laTFVEhUnSJ6ay-vQVhcgOPnPu8rS9QTElT-MrYOltcddtMvPP5rMTRU6xLXK_va9SA5EuspnudHHh37g

typed assembly language https://alastairreid.github.io/RelatedWork/notes/typed-assembly-language/ https://www.cs.cornell.edu/talc/papers.html Type-Safe Linking and Modular Assembly Language.

Seperate compilation for macros https://lexi-lambda.github.io/blog/2019/04/21/defeating-racket-s-separate-compilation-guarantee/ https://www.cs.utah.edu/plt/publications/macromod.pdf