"I'm currently more interested in building squishy cells."
I respect that, but just to get it written down, here's what I've come up with so far:
All lambda expressions must be lambda-lifted so they're at the top level of some module. (I guess this might count as a lambda-free logical framework.)
Every function type (X -> Y) is annotated as (X -> [C] Y) with the implementation code C of that function's source module. A simple export/import of an X-to-Y function will actually bind an import variable of the type (existscode C. (SatisfiesSignature S C * (X -> [C] Y))), where S is the import signature.
If a module has access to installed implementation code C and it knows SatisfiesSignature S C and SatisfiesSignature S C', then it can conclude C = C'. It can take advantage of this knowledge to get access to fuller knowledge about how an (X -> [C'] Y) function behaves.
"I was (and still am) waiting for you to teach them to me :p"
Really? I don't remember where we left off, but let's get in touch on this.