the propositions-as-types correspondence is ordinarily presented as linking the metatheory of typed lambda-calculi and the proof theory of intuitionistic logic. Griffin observed that this correspondence could be exten...
详细信息
ISBN:
(数字)9783319712376
ISBN:
(纸本)9783319712376
the propositions-as-types correspondence is ordinarily presented as linking the metatheory of typed lambda-calculi and the proof theory of intuitionistic logic. Griffin observed that this correspondence could be extended to classical logic through the use of control operators. this observation set off a flurry of further research, leading to the development of Parigot's lambda mu-calculus. In this work, we use the lambda mu-calculus as the foundation for a system of proof terms for classical first-order logic. In particular, we define an extended call-by-value lambda mu-calculus with a type system in correspondence with full classical logic. We extend the language with polymorphic types, add a host of data types in 'direct style', and prove several metatheoretical properties. All of our proofs and definitions are mechanised in Isabelle/HOL, and we automatically obtain an interpreter for a system of proof terms cum programming language-called mu ML-using Isabelle's code generation mechanism. Atop our proof terms, we build a prototype LCF-style interactive theorem prover-called mu TP- for classical first-order logic, capable of synthesising mu ML programs from completed tactic-driven proofs. We present example closed mu ML programs with classical tautologies for types, including some inexpressible as closed programs in the original lambda mu-calculus, and some example tactic-driven mu TP proofs of classical tautologies.
Smart contract applications on the blockchain can only reach their full potential if they integrate seamlessly with traditional software systems via a programmatic interface. this interface should provide for originat...
详细信息
ISBN:
(纸本)9783030890513;9783030890506
Smart contract applications on the blockchain can only reach their full potential if they integrate seamlessly with traditional software systems via a programmatic interface. this interface should provide for originating and invoking contracts as well as observing the state of the blockchain. We propose a typed API for this purpose and establish some properties of the combined system. Specifically, we provide an execution model that enables us to prove type-safe interaction between programs and the blockchain. We establish further properties of the model that give rise to requirements on the API. A prototype of the interface is implemented in OCaml for the Tezos blockchain.
programming heterogeneous systems has been greatly simplified by OpenCL, which provides a common low-level API for a large variety of compute devices. However, many low-level details, including data transfer, task sch...
详细信息
ISBN:
(纸本)9781479912841
programming heterogeneous systems has been greatly simplified by OpenCL, which provides a common low-level API for a large variety of compute devices. However, many low-level details, including data transfer, task scheduling, or synchronization, must still be managed by the application designer. Often, it is desirable to program heterogeneous systems in a higher-level language, making the developing process faster and less error-prone. In this paper, we introduce a framework to efficiently execute applications specified as synchronous dataflow graphs (SDF) on heterogeneous systems by means of OpenCL. In our approach, actors are embedded into OpenCL kernels and data channels are automatically instantiated to improve memory access latencies and end-to-end performance. the multi-level parallelism resulting from the hierarchical structure of heterogeneous systems is exploited by applying two techniques. Pipeline and task parallelism are used to distribute the application to the different compute devices and data-parallelism is used to concurrently process independent actor firings or even output tokens in a SIMD fashion. We demonstrate that the proposed framework can be used by application designers to efficiently exploit the parallelism of heterogeneous systems without writing low-level architecture dependent code.
A hardware/software co-designed processor transparently supports a ubiquitous ISA (e.g. x86) with diversified and innovative microarchitectural implementations. It leverages co-designed HW features and dynamic binary ...
详细信息
ISBN:
(纸本)9781467355254;9781467355247
A hardware/software co-designed processor transparently supports a ubiquitous ISA (e.g. x86) with diversified and innovative microarchitectural implementations. It leverages co-designed HW features and dynamic binary translation (DBT) SW to morph existing binary programs to scale performance and save power. On such systems, the portable bytecode of modern dynamic languages (e.g. Java, JavaScript, etc.) is first translated into the code in the architecture ISA by the just-in-time (JIT) compilation in the bytecode virtual machine, and then into the code in the internal implementation ISA by the DBT. this not only incurs the translation overheads twice, but also brings significant emulation inefficiency as the DBT does not have the high level bytecode information. In this paper, we present AccelDroid, which accelerates the Android Dalvik bytecode execution on the HW/SW co-designed processor through direct bytecode translation in the DBT. Our experiments on a HW/SW co-designed Transmeta Efficeon machine show that AccelDroid can improve performance by 78% and save energy by 40% for the CaffeineMark 3.0 benchmark suite.
this book constitutes the refereed proceedings of the 11th International symposium on Automated Technology for Verification and Analysis, ATVA 2013, held at Hanoi, Vietnam, in October 2013. the 27 regular papers, 3 sh...
详细信息
ISBN:
(数字)9783319024448
ISBN:
(纸本)9783319024431
this book constitutes the refereed proceedings of the 11th International symposium on Automated Technology for Verification and Analysis, ATVA 2013, held at Hanoi, Vietnam, in October 2013.
the 27 regular papers, 3 short papers and 12 tool papers presented together with 3 invited talks were carefully selected from73 submissions.
the papers are organized in topical, sections on analysis and verification of hardware circuits, systems-on-chip and embedded systems, analysis of real-time, hybrid, priced/weighted and probabilistic systems, deductive, algorithmic, compositional, and abstraction/refinement techniques for analysis and verification, analytical techniques for safety, security, and dependability, testing and runtime analysis based on verification technology, analysis and verification of parallel and concurrent hardware/software systems, verification in industrial practice, and applications and case studies.
ABS (for abstract behavioral specification) is a novel language for modeling feature-rich, distributed, object-oriented systems at an abstract, yet precise level. ABS has a clear and simple concurrency model that perm...
详细信息
In this paper the author presents a generic test equipment for embedded platform software. this approach helps to overcome the paradigms of modern software development like object-oriented concepts, rapid prototyping ...
详细信息
In this paper the author presents a generic test equipment for embedded platform software. this approach helps to overcome the paradigms of modern software development like object-oriented concepts, rapid prototyping and communication-support over a large number of different protocols. As different platforms are supported, the most relevant differences between compilers, processors and operating systems are described. Since testers of embedded systems are usually familiar with C and C++, the test equipment is based on CINT, a C++ interpreter. the last section of this paper investigates the advantages and drawbacks of CINT.
暂无评论