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) -
Formalizing Constructive Quantifier Elimination in Agda
অনুযায়ী: Jeremy Pope
প্রকাশিত: (2018-07-01)