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)