curry-agda

This repository contains Agda libraries and examples to prove properties of operations defined in Curry.

The ideas behind these libraries and proofs are discussed in this paper.

The Agda proofs require the Iowa Agda Library.

The recent Curry distributions PAKCS and KiCS2 contain automatic translator from Curry into the format of these proofs.

Contents:

• nondet: This directory contains the libraries (nondet.agda and nondet-thms.agda) and proofs for the set of values representation of non-determinism in Agda.
• choices: This directory contains the proofs for the planned choices representation of non-determinism in Agda.