AK
A.W. Kierska
info
Please Note
<p>This page displays the records of the person named above and is not linked to a unique person identifier. This record may need to be merged to a profile.</p>
1 records found
1
Specified Agda is Testable Haskell
Translating Agda Postconditions to QuickCheck Property Tests in agda2hs
Formally verified code written in dependently typed languages can be integrated into larger, non-verified code bases through source-to-source translation. The agda2hs compiler enables such integration by translating verified Agda code to readable Haskell, erasing proofs and type indices in the process. The properties that a program is verified against are encoded as such proofs and type indices, and are therefore also erased. Yet being able to check these properties is important: in the agda2hs workflow, verified code may depend on unverified Haskell libraries whose properties are assumed without proof and never tested.
In this paper, we present an extension to agda2hs that extracts postconditions and translates them into Haskell QuickCheck property tests. Since postconditions in Agda are encoded at the type level, they are not executable and cannot be translated to Haskell directly. We address this by deriving semi-decision procedures that check whether a proposition holds for given inputs. We cover postconditions expressed as separate lemmas, sigma types, and indexed datatypes. We implement lemma-to-test translation as a working agda2hs extension; it requires the user to write the decision procedure by hand. We present the automatic derivation of such procedures as an algorithm design with worked examples. ...
In this paper, we present an extension to agda2hs that extracts postconditions and translates them into Haskell QuickCheck property tests. Since postconditions in Agda are encoded at the type level, they are not executable and cannot be translated to Haskell directly. We address this by deriving semi-decision procedures that check whether a proposition holds for given inputs. We cover postconditions expressed as separate lemmas, sigma types, and indexed datatypes. We implement lemma-to-test translation as a working agda2hs extension; it requires the user to write the decision procedure by hand. We present the automatic derivation of such procedures as an algorithm design with worked examples. ...
Formally verified code written in dependently typed languages can be integrated into larger, non-verified code bases through source-to-source translation. The agda2hs compiler enables such integration by translating verified Agda code to readable Haskell, erasing proofs and type indices in the process. The properties that a program is verified against are encoded as such proofs and type indices, and are therefore also erased. Yet being able to check these properties is important: in the agda2hs workflow, verified code may depend on unverified Haskell libraries whose properties are assumed without proof and never tested.
In this paper, we present an extension to agda2hs that extracts postconditions and translates them into Haskell QuickCheck property tests. Since postconditions in Agda are encoded at the type level, they are not executable and cannot be translated to Haskell directly. We address this by deriving semi-decision procedures that check whether a proposition holds for given inputs. We cover postconditions expressed as separate lemmas, sigma types, and indexed datatypes. We implement lemma-to-test translation as a working agda2hs extension; it requires the user to write the decision procedure by hand. We present the automatic derivation of such procedures as an algorithm design with worked examples.
In this paper, we present an extension to agda2hs that extracts postconditions and translates them into Haskell QuickCheck property tests. Since postconditions in Agda are encoded at the type level, they are not executable and cannot be translated to Haskell directly. We address this by deriving semi-decision procedures that check whether a proposition holds for given inputs. We cover postconditions expressed as separate lemmas, sigma types, and indexed datatypes. We implement lemma-to-test translation as a working agda2hs extension; it requires the user to write the decision procedure by hand. We present the automatic derivation of such procedures as an algorithm design with worked examples.