Algebra of Programming in Agda: Dependent Types for Relational Program Derivation
<p>Relational program derivation is the technique of stepwise refining a relational specification to a program by algebraic rules. The program thus obtained is correct by construction. Meanwhile, dependent type theory is rich enough to express various correctness properties to be verified by t...
المؤلفون الرئيسيون: | Mu, S, Ko, H, Jansson, P |
---|---|
التنسيق: | Journal article |
منشور في: |
2009
|
مواد مشابهة
-
Algebra of Programming using Dependent Types
حسب: Mu, S, وآخرون
منشور في: (2008) -
MiniAgda: Integrating Sized and Dependent Types
حسب: Andreas Abel
منشور في: (2010-12-01) -
Certified Context-Free Parsing: A formalisation of Valiant's Algorithm in Agda
حسب: Jean-Philippe Bernardy, وآخرون
منشور في: (2016-06-01) -
Proving Non-Deterministic Computations in Agda
حسب: Sergio Antoy, وآخرون
منشور في: (2017-01-01) -
Trace and Stable Failures Semantics for CSP-Agda
حسب: Bashar Igried, وآخرون
منشور في: (2017-09-01)