Andrew M. Mironov
In the paper we introduce graphical objects (called state diagrams) related to functional programs. It is shown that state diagrams of functional programs can be used to solve problems of verification of functional programs. The proposed approach is illustrated by an example of verification of a sorting program.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
A Diagrammatic Algebra for Program Logics
本文通过引入带 $\oplus$ 上迹的带图和 Kleene-Cartesian 双范畴，为命令式程序提供了一种图解记法与证明系统，其表达能力至少与 Hoare 逻辑相当。
We introduce a novel framework, termed $λ$DD, that revisits Binary Decision Diagrams from a purely functional point of view. The framework allows to classify the already existing variants, including the most recent ones like Chain-DD and ESRBDD, as implementations of a special class of ordered models. We enumerate, in a principled way, all the models of this class and isolate its most expressive model. This new model, termed $λ$DD-O-NUCX, is suitable for both dense and sparse Boolean functions, and is moreover invariant by negation. The canonicity of $λ$DD-O-NUCX is formally verified using the…
Along the lines of the Abramsky ``Proofs-as-Processes'' program, we present an interpretation of multiplicative linear logic as typing system for concurrent functional programming. In particular, we study a linear multiple-conclusion natural deduction system and show it is isomorphic to a simple and natural extension of $λ$-calculus with parallelism and communication primitives, called $λ_{\unicode{8523}}$. We shall prove that $λ_{\unicode{8523}}$ satisfies all the desirable properties for a typed programming language: subject reduction, progress, strong normalization and confluence.
Calculating risk in functional programming
在容忍硬件不可靠性的趋势下，准确性被用来换取成本节约。在不太可靠的机器上运行，“功能正确”的代码变得有风险，人们需要知道风险是如何传播的，以减轻它。然而，风险估计似乎超出了普通程序员的技术能力和核心实践。在本文中，我们建议，风险建设性地处理在功能性编程（a）编写程序，可以选择预期和错误的行为，并通过（b）推理他们在线性代数扩展到标准，一个香格里拉Bird-Moor代数编程。特别是，传播的故障在标准的程序转换技术称为元组和融合计算，使故障的整体表示的故障的部分。
We report on the automation of a technique to prove the correctness of program transformations in higher-order program calculi which may permit recursive let-bindings as they occur in functional programming languages. A program transformation is correct if it preserves the observational semantics of programs. In our LRSX Tool the so-called diagram method is automated by combining unification, matching, and reasoning on alpha-renamings on the higher-order meta-language, and automating induction proofs via an encoding into termination problems of term rewrite systems. We explain the techniques, …
A New Method of Verification of Functional Programs
本文研究了字符串上函数程序的验证问题，其中函数程序的性质规范由其它函数程序定义，一个函数程序S1满足另一个函数程序S2定义的规范当且仅当由函数程序S1和S2定义的函数的组合等于常数1.我们引入了一个FP的状态图的概念，并减少了验证问题的FP的状态图的分析问题。所提出的方法是说明了一个排序程序的验证的例子。
This is a draft of the textbook/monograph that presents computability theory using string diagrams. The introductory chapters have been taught as graduate and undergraduate courses and evolved through 8 years of lecture notes. The later chapters contain new ideas and results about categorical computability and some first steps into computable category theory. The underlying categorical view of computation is based on monoidal categories with program evaluators, called *monoidal computers*. This categorical structure can be viewed as a single-instruction diagrammatic programming language called…
Proof-Producing Translation of Functional Programs into a Time \& Space Reasonable Model
提出半自动化框架，将Isabelle/HOL子集中的尾递归函数翻译为深度嵌入的while程序，该模型模拟图灵机仅需二次时间与常数空间开销，是首个面向时间空间合理计算模型的框架。
Encoding High-level Quantum Programs as SZX-diagrams
本文提出一种将线性依赖类型语言 Proto-Quipper-D 片段中的量子程序编码为 SZX 图的方法，并证明该编码能使图规模随程序大小线性增长。
The (Lazy) Functional Side of Logic Programming
将逻辑程序转换成功能程序的可能性一直是研究的课题。许多方法的共同点是，原始逻辑程序，为了被翻译，需要被良好地模态化，这导致了这样的共识，即这些程序可以被认为是逻辑程序的“功能部分”。因此，“复杂”逻辑变量、动态选择规则的可能性以及非良模程序的一般属性是逻辑程序的独有特征，这一点已被广泛接受。这并不完全正确，因为其中一些特性在惰性函数式语言中自然存在。我们通过定义一个适用于更广泛的逻辑程序的简单翻译，重新讨论了什么功能是逻辑编程范式所独有的老问题，并证明了目前的界限是不合理的限制。
This volume constitutes the pre-proceedings of the 26th International Workshop on Functional and Logic Programming (WFLP 2018). It is formed of those papers selected by the program committee for presentation at the workshop. After discussion at the workshop, the program committee will select a number of papers to be invited for the second round of refereeing and selection for the formal proceedings.
HMC: Verifying Functional Programs Using Abstract Interpreters
我们提出了Hindley-Milner-Cousots（HMC），一个算法，允许任何一阶命令式程序的过程间分析被用来验证类型化高阶函数程序的安全属性。HMC工作如下。首先，它利用函数程序的类型结构来生成一组逻辑精化约束，这些约束的满足意味着源程序的安全性。其次，它将逻辑精化约束转换成一个简单的一阶命令式程序，该程序是安全的，当且仅当约束是可满足的。因此，HMC一举使工具的不变生成，例如，基于抽象域、谓词抽象、反例引导的精化和Craig插值可以直接应用于以全自动的方式验证现代函数式语言的安全属性。我们已经实现了HMC，并描述了初步的实验结果，使用两个命令式检查器- ARMC和InterProc -来验证OCaml程序。因此，通过组成基于类型的推理在程序语法和基于状态的推理在抽象解释的基础上，HMC打开了大门，以现代程序设计语言编写的程序的自动验证。
Functional Logic Programming with Generalized Circular Coinduction
我们提出了一种方法，以适应功能逻辑编程处理推理coinductively解释的程序，以及归纳解释的程序。为了做到这一点，我们考虑一类有趣的对象，这种共归纳的解释，即正规条款。我们展示了如何通常的数据结构可以适应捕捉这些对象。我们采用Curry的操作语义来解释程序。我们用几个例子来说明这种方法，这些例子显示了我们的方法的工作原理和几种情况下，它可能是有用的。最后，我们建议如何声明性语义可以适当地适应。
foetus -- Termination Checker for Simple Functional Programs
本研究提出带终止性检查器的函数式语言foetus，通过提取函数调用、补全调用图并寻找参数良基结构序，来证明简单函数式程序的终止性。
Forward slicing of functional logic programs by partial evaluation
程序切片主要是在命令式语言的背景下研究的，它已被应用到各种各样的软件工程任务，如程序理解，维护，调试，测试，代码重用等。这项工作介绍了第一个前向切片技术的声明性多范式程序，集成功能和逻辑编程的功能。基本上，给定一个程序和一个切片标准（在我们的设置中是一个函数调用），计算出的前向切片包含了原始程序中从切片标准可以到达的那些部分。我们的程序切片方法是基于（在线）部分评估的扩展。因此，它提供了一个简单的方法来开发程序切片工具，从现有的部分评估器，并有助于澄清这两种方法之间的关系。一个切片工具的多范式语言咖喱，这表明了我们的方法的有用性，已经实现了咖喱本身。
Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order (Long Version)
我们展示了如何高阶函数程序的复杂性可以自动分析，通过应用程序转换到一个去功能化的版本，他们，并将结果反馈给现有的工具的复杂性分析的一阶长期重写系统。这样做的同时仔细分析复杂性保存和反射的转换，使所获得的长期重写系统的复杂性反映在初始程序的复杂性。此外，我们描述了合适的策略的应用研究的转换，并提供了充足的实验数据，以评估我们的方法的可行性。
Relational cost analysis aims at formally establishing bounds on the difference in the evaluation costs of two programs. As a particular case, one can also use relational cost analysis to establish bounds on the difference in the evaluation cost of the same program on two different inputs. One way to perform relational cost analysis is to use a relational type-and-effect system that supports reasoning about relations between two executions of two programs. Building on this basic idea, we present a type-and-effect system, called ARel, for reasoning about the relative cost of array-manipulating,…
String Diagrams for $λ$-calculi and Functional Computation
本教程以系统方式介绍高阶计算的字符串图与图语言，从范畴论概念的二维语法逐步深入到笛卡尔闭范畴，通过从范畴模型重构分层超图语法并探讨其在编程语言领域的应用。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。