Sökning: WFRF:(Johansson Moa 1981) >
Proving Type Class ...
Proving Type Class Laws for Haskell
-
- Arvidsson, Andreas (författare)
- Chalmers tekniska högskola,Chalmers University of Technology
-
- Johansson, Moa, 1981 (författare)
- Chalmers tekniska högskola,Chalmers University of Technology
-
- Touche, Robin (författare)
- Chalmers tekniska högskola,Chalmers University of Technology
-
(creator_code:org_t)
- 2019-02-21
- 2019
- Engelska.
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. ; 10447 LNCS, s. 61-74
- Relaterad länk:
-
http://arxiv.org/pdf...
-
visa fler...
-
https://research.cha...
-
https://doi.org/10.1...
-
visa färre...
Abstract
Ämnesord
Stäng
- Type classes in Haskell are used to implement ad-hoc polymorphism, i.e. a way to ensure both to the programmer and the compiler that a set of functions are defined for a specific data type. All instances of such type classes are expected to behave in a certain way and satisfy laws associated with the respective class. These are however typically just stated in comments and as such, there is no real way to enforce that they hold. In this paper we describe a system which allows the user to write down type class laws which are then automatically instantiated and sent to an inductive theorem prover when declaring a new instance of a type class.
Ämnesord
- NATURVETENSKAP -- Matematik -- Algebra och logik (hsv//swe)
- NATURAL SCIENCES -- Mathematics -- Algebra and Logic (hsv//eng)
- MEDICIN OCH HÄLSOVETENSKAP -- Medicinsk bioteknologi -- Biomedicinsk laboratorievetenskap/teknologi (hsv//swe)
- MEDICAL AND HEALTH SCIENCES -- Medical Biotechnology -- Biomedical Laboratory Science/Technology (hsv//eng)
- NATURVETENSKAP -- Matematik -- Matematisk analys (hsv//swe)
- NATURAL SCIENCES -- Mathematics -- Mathematical Analysis (hsv//eng)
Nyckelord
- Ad-hoc polymorphism
- Program compilers
Publikations- och innehållstyp
- kon (ämneskategori)
- ref (ämneskategori)
Hitta via bibliotek
Till lärosätets databas