Full Abstraction for Free

Marco PaviottiNicolas Wu

Mar 2023

摘要

Structured recursion schemes such as folds and unfolds have been widely usedfor structuring both functional programs and program semantics. In thiscontext, it has been customary to implement denotational semantics as foldsover an inductive data type to ensure termination and compositionality.Separately, operational models can be given by unfolds, and naturally not alloperational models coincide with a given denotational semantics in a meaningfulway. To ensure these semantics are coherent it is important to consider theproperty of full abstraction which relates the denotational and the operationalmodel. In this paper, we show how to engineer a compositional semantics suchthat full abstraction comes for free. We do this by using distributive lawsfrom which we generate both the operational and the denotational model. Thedistributive laws ensure the semantics are fully abstract at the type level,thus relieving the programmer from the burden of the proofs.

展开全部

图表提取

论文十问

参考文献

被引用

提问与回答

暂无人提供速读十问回答

被引用

笔记

问答

领域