Oh, this is great. Sorry I missed that in my related work section :/
That's a great point! I actually discuss Czar in the paper, as part of my discussion of structured proofs: Calculational, structured, and declarative proofs The tactic-based proof style pioneered by LCF [LCF+Gordon1979]…
Oh, this is great. Sorry I missed that in my related work section :/
That's a great point! I actually discuss Czar in the paper, as part of my discussion of structured proofs: Calculational, structured, and declarative proofs The tactic-based proof style pioneered by LCF [LCF+Gordon1979]…