Foundational Certification of Code Transformations Using Automatic Differentiation | Zendy

Tadjouddine Emmanuel | Zendy; Lv Wenjin | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Foundational Certification of Code Transformations Using Automatic Differentiation

Author(s) -

Tadjouddine Emmanuel,

Lv Wenjin

Publication year - 2014

Publication title -

computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.145

H-Index - 5

eISSN - 2300-7036

pISSN - 1508-2806

DOI - 10.7494/csci.2014.15.2.215

Subject(s) - computer science , hoare logic , correctness , programming language , certification , mathematical proof , separation logic , function (biology) , axiomatic semantics , rule of inference , inference , code (set theory) , process (computing) , theoretical computer science , operational semantics , semantics (computer science) , artificial intelligence , denotational semantics , evolutionary biology , law , set (abstract data type) , geometry , mathematics , political science , biology

Automatic Differentiation (AD) is concerned with the semantics augmentation of an input program representing a function to form a transformed program that computes the function's derivatives. To ensure the correctness of the AD transformed code, particularly for safety critical applications, we aim at certifying the algebraic manipulations at the heart of the AD process. We have considered a WHILE-language and have shown how such proofs can be constructed by using an appropriate relational Hoare logic.In particular, we have shown how such inference rules can be constructed for both the forward and reverse mode AD by using an abductive logical reasoning

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research