Algebra of Programming in Agda: Dependent Types for Relational Program Derivation

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...

Cur síos iomlán

Sonraí bibleagrafaíochta
Príomhchruthaitheoirí:	Mu, S, Ko, H, Jansson, P
Formáid:	Journal article
Foilsithe / Cruthaithe:	2009

Míreanna comhchosúla

Algebra of Programming using Dependent Types
de réir: Mu, S, et al.
Foilsithe / Cruthaithe: (2008)

MiniAgda: Integrating Sized and Dependent Types
de réir: Andreas Abel
Foilsithe / Cruthaithe: (2010-12-01)

Certified Context-Free Parsing: A formalisation of Valiant's Algorithm in Agda
de réir: Jean-Philippe Bernardy, et al.
Foilsithe / Cruthaithe: (2016-06-01)

Proving Non-Deterministic Computations in Agda
de réir: Sergio Antoy, et al.
Foilsithe / Cruthaithe: (2017-01-01)

Trace and Stable Failures Semantics for CSP-Agda
de réir: Bashar Igried, et al.
Foilsithe / Cruthaithe: (2017-09-01)

Towards an Extrinsic Formalization of Featherweight Java in Agda
de réir: Samuel Feitosa, et al.
Foilsithe / Cruthaithe: (2021-12-01)

Thingifying Neda: The Construction of Commemorative and Affective Thingifications of Neda Agda Soltan
de réir: Carsten Stage
Foilsithe / Cruthaithe: (2011-10-01)

Entre o céu e as caldeiras: espectros desconstrutivos em “Agda”, de Hilda Hilst
de réir: Lilia Lomam
Foilsithe / Cruthaithe: (2024-05-01)

Entre o céu e as caldeiras: espectros desconstrutivos em “Agda”, de Hilda Hilst
de réir: Lilia Loman
Foilsithe / Cruthaithe: (2017-02-01)

İki Boyutlu Sığ Akım Denklemlerinin Sırasız Ağda Sayısal Çözümü için Bilgisayar Yazılımı Geliştirilmesi
de réir: Nuray Öktem
Foilsithe / Cruthaithe: (2018-04-01)

Algebra : programmed /
de réir: 385109 Alwin, Robert H., et al.
Foilsithe / Cruthaithe: (1978)

”Året präglades av coronaviruspandemin” – Regeringar rapporterar om statligt ägda bolag i Finland och Sverig
de réir: Merja Koskela, et al.
Foilsithe / Cruthaithe: (2022-12-01)

The Algebra of Programming
de réir: Bird, R, et al.
Foilsithe / Cruthaithe: (1996)

Algebraic and logic programming /
de réir: Grabowski, J., et al.
Foilsithe / Cruthaithe: (1988)

Program Algebra for Turing-Machine Programs
de réir: Jan A. Bergstra, et al.
Foilsithe / Cruthaithe: (2019-12-01)

Algebra of Logic Programming
de réir: Seres, S, et al.
Foilsithe / Cruthaithe: (1999)

Algebra of Logic Programming
de réir: Seres, S, et al.
Foilsithe / Cruthaithe: (1999)

Program Algebra for Random Access Machine Programs
de réir: Cornelis Middelburg
Foilsithe / Cruthaithe: (2022-12-01)

Type theory as a framework for modelling and programming
de réir: Ionescu, C, et al.
Foilsithe / Cruthaithe: (2018)

Algebraic Identities for Program Calculation
de réir: Bird, R
Foilsithe / Cruthaithe: (1989)

On strongest algebraic program invariants
de réir: Hrushovski, E, et al.
Foilsithe / Cruthaithe: (2023)

A programmed vector algebra/
de réir: 171030 Gardner, K. L.
Foilsithe / Cruthaithe: (1969)

Beginning algebra : an individualized program /
de réir: 386042 Drooyan, Irving, et al.
Foilsithe / Cruthaithe: (1978)

Combining dependent annotations for relational algebra
de réir: Kostylev, E, et al.
Foilsithe / Cruthaithe: (2012)

Equivalence of the schemes of programs based on the algebraic approach to setting the semantics of programming languages
de réir: Y. P. Korablin
Foilsithe / Cruthaithe: (2022-03-01)

Relational algebraic ornaments
de réir: Ko, H, et al.
Foilsithe / Cruthaithe: (2013)

Program synthesis with algebraic library specifications
de réir: Mariano, Benjamin, et al.
Foilsithe / Cruthaithe: (2021)

An algebraic transformation system for occam programs
de réir: Goldsmith, M, et al.
Foilsithe / Cruthaithe: (1987)

Applied mathematics for technical programs : algebra /
de réir: 406122 Moon, Robert G.
Foilsithe / Cruthaithe: (1973)

Matrix algebra : a programmed introduction /
de réir: Dorf, Richard C. 388440
Foilsithe / Cruthaithe: (1969)

A programmed course in basic algebra /
de réir: 334633 Beck, William C., et al.
Foilsithe / Cruthaithe: (1971)

Ninth colloquium on trees in algebra and programming
Foilsithe / Cruthaithe: (1984)

The Essentials of Clifford Algebras with Maple Programming
de réir: Mutlu Akar
Foilsithe / Cruthaithe: (2021-04-01)

About Algebraic Program Models with Procedures
de réir: R. I. Podlovchenko, et al.
Foilsithe / Cruthaithe: (2015-03-01)

About Algebraic Program Models with Procedures
de réir: R. I. Podlovchenko, et al.
Foilsithe / Cruthaithe: (2012-01-01)

Numerical algebraic geometry and semidefinite programming
de réir: Jonathan D. Hauenstein, et al.
Foilsithe / Cruthaithe: (2021-08-01)

Type A Hecke algebras and related algebras
de réir: Erdmann, K
Foilsithe / Cruthaithe: (2004)

Program Let’s Algebraize 1.0 bimbing pelajar minat Algebra
de réir: Ibrahim, Siti Nur Iqmal
Foilsithe / Cruthaithe: (2022)

Verifying Higher−Order Functional Programs with Pattern Matching Algebraic Data Types
de réir: Ong, C, et al.
Foilsithe / Cruthaithe: (2011)

Verifying Higher-Order Functional Programs with Pattern-Matching Algebraic Data Types
de réir: Ong, C, et al.
Foilsithe / Cruthaithe: (2011)