A Versatile, Sound Tool for Simplifying Definitions
We present a tool, simplify-defun, that transforms the definition of a given function into a simplified definition of a new function, providing a proof checked by ACL2 that the old and new functions are equivalent. When appropriate it also generates termination and guard proofs for the new function. We explain how the tool is engineered so that these proofs will succeed. Examples illustrate its utility, in particular for program transformation in synthesis and verification.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Learning Higher-Order Programs without Meta-Interpretive Learning
Learning complex programs through inductive logic programming (ILP) remains a formidable challenge. Existing higher-order enabled ILP systems show improved accuracy and learning performance, though remain hampered by the…
Inductive logic programmingSome clues to build a sound analysis relevant to hearing
Analysis tools used in research laboratories, for sound synthesis, by musicians or sound engineers can be rather different. Discussion of the assumptions and of the limitations of these tools permits to propose a first t…
Ultrawideband USRP-Based Channel Sounding Utilizing the RFNoC Framework
This paper shows how an ultrawideband channel sounder can be built with the latest National Instruments (NI) Universal Software Radio Peripheral (USRP) equipment, featuring onboard FPGA processing and utilizing open-sour…
Simplifying Causality: A Brief Review of Philosophical Views and Definitions with Examples from Economics, Education, Medicine, Policy, Physics and Engineering
This short paper compiles the big ideas behind some philosophical views, definitions, and examples of causality. This collection spans the realms of the four commonly adopted approaches to causality: Humes regularity, co…
Causal InferencecounterfactualBundleSeg: A versatile, reliable and reproducible approach to white matter bundle segmentation
This work presents BundleSeg, a reliable, reproducible, and fast method for extracting white matter pathways. The proposed method combines an iterative registration procedure with a recently developed precise streamline …
ClusteringSegmentationSensitivitySpecificity