[tlaplus] Using TLA+ for Simulation-proofs

[Mike Clark <undefinedspace@xxxxxxxxx>]

Hi all,

I'm just beginning to learn about TLA+ and trying to understand some of the capabilities it provides and the problems it could be used to solve.

I'm curious if TLA+ could be used for specifying simulation-proofs (e.g., https://eccc.weizmann.ac.il/report/2017/112/). 

I haven't seen much about such a use case discussed online. If it could be used for something like this, any pointers? I'm especially interested in computational indistinguishability in the real/ideal world paradigm.

Mike

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7311211f-1c54-4225-8f2a-af18f3e2e57bn%40googlegroups.com.