COQ'S FUNCTIONAL PROGRAMMING LANGUAGE

REVISED: Tuesday, November 5, 2024

1. COQ'S FUNCTIONAL PROGRAMMING LANGUAGE

We type in the CoqIDF buffer window using Coq keyword vernacular commands.

As shown below, the Inductive type day : is defined to be := the list of day items or constructors separated by | vertical bars. The list of constructors ends with a period .

Inductive day : Type :=

    | monday

    | tuesday

    | wednesday

    | thursday

    | friday

    | saturday

    | sunday.

We move the cursor to the right of the period and click the CoqIDE down-arrow to compile the above Type.  If the compile is successful the line color changes to green.

After the successful compile, CoqIDE responds in the Messages' window with 

day is defined

day_rect is defined

day_ind is defined

day_rec is defined

day_sind is defined

Next, we write the function next_weekday based on the above day type. The function uses pattern matching, matching the argument d and the branch or case type it returns will be : day type. The branch or case is separated by right arrows pointing to the matching argument. The function ends with end and a period .

Definition next_weekday (d:day) : day :=

    match d with

    | monday    => tuesday

    | tuesday   => wednesday

    | wednesday => thursday

    | thursday  => friday

    | friday    => monday

    | saturday  => monday

    | sunday    => monday

    end.

We move the cursor to the right of the period after end and click the CoqIDE down-arrow to compile the function next_weekday.  If the compile is successful the function color changes to green.

After the successful compile, CoqIDE responds in the Messages' window with 

next_weekday is defined

To call a function, we use the vernacular command Compute.

Compute (next_weekday friday).

After the successful compile, CoqIDE responds in the Messages window with

    = monday

     : day

We test our next_weekday function using the vernacular command Example.

Example test_next_weekday :

    (next_weekday (next_weekday saturday)) = tuesday.

After a successful compile, CoqIDE responds in the Goal's window by telling us we must first prove the new test_next_weekday function before we can use it. 

1 goal

______________________________________(1/1)

next_weekday (next_weekday saturday) =

tuesday

CoqIDF wants us to prove 1 goal the test_next_weekday function.

We use the simpl tactic to simplify the goal we are trying to prove. 

Proof. simpl. reflexivity. Qed.

After Proof we compile period by period one at a time. After the successful compile of  simple,  CoqIDE responds in the Goal's window with 

1 goal

______________________________________(1/1)

tuesday = tuesday

Notice 1 goal has changed, now both sides of = are the same.

When both sides of = are the same we can use the tactic reflexivity. After the successful compile of  reflexivity, CoqIDE responds in the Goal's window with 

No more goals.

Now when we compile Qed. all windows are blank and CoqIDE accepts the Proof as proven.

Compute (next_weekday (next_weekday saturday)).

After the successful compile, CoqIDE responds in the Messages window with

    = tuesday

     : day

Notice the above Compute is passing function arguments from right to left. For example, next_weekday saturday computes to monday which is passed as an argument to the function on the left next_weekday which uses it to compute the final answer tuesday.

2. CONCLUSION 

The Coq functional programming Language is easy to use.

3. REFERENCES

Bird, R. (2015). Thinking Functionally with Haskell. Cambridge, England: Cambridge University Press.

Davie, A. (1992). Introduction to Functional Programming Systems Using Haskell. Cambridge, England: Cambridge University Press.

Goerzen, J. & O'Sullivan, B. &  Stewart, D. (2008). Real World Haskell. Sebastopol, CA: O'Reilly Media, Inc.

Hutton, G. (2007). Programming in Haskell. New York: Cambridge University Press.

Lipovača, M. (2011). Learn You a Haskell for Great Good!: A Beginner's Guide. San Francisco, CA: No Starch Press, Inc.

Thompson, S. (2011). The Craft of Functional Programming. Edinburgh Gate, Harlow, England: Pearson Education Limited.

CALCULUS of INDUCTIVE CONSTRUCTIONS (CIC) and Gallina

REVISED: Wednesday, October 30, 2024

1. The Calculus of Inductive Constructions (CIC)

CIC is a powerful type of theory that serves as the foundation for the Coq proof assistant. It's a higher-order logic system where types and terms are unified, allowing for a seamless integration of logic and computation.

Key Features

Types and Terms:

In CIC, types and terms are not distinct entities. Both are represented as expressions within the same language. This means that types can be the subjects of proofs, and proofs can be the objects of computation.

Dependent Types: 

CIC supports dependent types, where the type of an expression can depend on the value of another expression. This enables fine-grained reasoning about complex data structures and algorithms.

Inductive Types: 

Inductive types allow the definition of recursive data structures, such as natural numbers, lists, and trees. This is crucial for defining algorithms and proving properties about them.

Proofs as Programs: 

The Curry-Howard isomorphism, a fundamental principle in CIC, establishes a correspondence between proofs and programs. This means that proofs can be seen as programs that construct values of a certain type, and programs can be seen as proofs of their correctness.

2. Gallina

Gallina is a high-level specification language built on top of CIC. It provides a more user-friendly syntax and a rich set of features for writing mathematical proofs and formal specifications.

Key Features

Intuitive Syntax: 

Gallina uses a more natural syntax compared to raw CIC, making it easier to read and write.

Tactics: 

Gallina provides a variety of tactics for constructing proofs interactively. These tactics automate common proof steps, reducing the amount of manual effort required.

Inductive Definitions: 

Gallina allows for the definition of inductive types and functions using a concise and intuitive syntax.

Higher-Order Logic: 

Gallina supports higher-order logic, allowing for reasoning about functions and predicates.

3. How Gallina and CIC Work Together

Key Features

Specification: 

The user writes a formal specification in Gallina, defining the properties and theorems to be proven.

Proof Development: 

The user interacts with the Coq proof assistant to construct proofs interactively. Gallina provides a convenient interface for this process.

Type Checking: 

Coq's type checker ensures the correctness of the proof by verifying that each step adheres to the rules of CIC.

Proof Completion: 

Once a proof is completed, Coq generates a formal proof object, which can be machine-checked for correctness.

4. Benefits of Using CIC and Gallina

Key Features

Formal Verification: 

CIC and Gallina enable the formal verification of software and hardware systems, ensuring their correctness and reliability.

Mathematical Reasoning: 

CIC can be used to formalize and reason about complex mathematical concepts, such as number theory, algebra, and topology.

Program Synthesis: 

The Curry-Howard isomorphism allows for the synthesis of programs from proofs, leading to the development of correct-by-construction software.

Education and Research: 

CIC and Gallina are powerful tools for teaching and researching formal methods, logic, and programming languages.

5. CONCLUSION

CIC and Gallina provide a robust framework for formal reasoning and program verification. By combining the power of higher-order logic, dependent types, and inductive definitions, they enable the development of complex mathematical theories and the rigorous verification of software systems.

6. REFERENCES

Bird, R. (2015). Thinking Functionally with Haskell. Cambridge, England: Cambridge University Press.

Davie, A. (1992). Introduction to Functional Programming Systems Using Haskell. Cambridge, England: Cambridge University Press.

Goerzen, J. & O'Sullivan, B. &  Stewart, D. (2008). Real World Haskell. Sebastopol, CA: O'Reilly Media, Inc.

Hutton, G. (2007). Programming in Haskell. New York: Cambridge University Press.

Lipovača, M. (2011). Learn You a Haskell for Great Good!: A Beginner's Guide. San Francisco, CA: No Starch Press, Inc.

Thompson, S. (2011). The Craft of Functional Programming. Edinburgh Gate, Harlow, England: Pearson Education Limited.

COQ

REVISED: Tuesday, October 29, 2024

1. INTRODUCTION

Imagine you're building a really cool LEGO structure. You have all the bricks and pieces, and you have a plan (instructions) on how to build it. Coq is like a super smart friend who helps you make sure you're following the plan perfectly and that your LEGO structure is strong and sturdy.

Here's how it works:

Proof Assistant:

Coq is a proof assistant. That means it helps you write proofs, which are like arguments or explanations that show something is true.

Math and Programming:

Coq can be used for math and programming. In math, it can help you prove theorems, like proving that 2 + 2 always equals 4. In programming, it can help you write programs that are correct and work the way they should.

Formal Verification:

Coq is used for formal verification. This means it can check if your math or programming is correct, just like your friend checks your LEGO building.

So, Coq is a powerful tool that helps people be sure that their math and programming is accurate and reliable. It's like having a super-smart friend who can help

2. COQIDE

Imagine CoqIDE as a special kind of word processor, but instead of writing stories or essays, it helps you build logical arguments and proofs. It's like having a super smart friend who can check your work and tell you if your reasoning is correct.

Here's what it does:

Proof Editing:

You can type in your proofs, and CoqIDE will help you by suggesting steps or pointing out mistakes.

Auto-Completion: 

It can finish your sentences for you, just like your phone does when you text!

Highlighting: 

It highlights important parts of your proof to make it easier to read and understand.

Checking: 

CoqIDE checks your proof step-by-step to make sure it's logically sound.

So, CoqIDE is a tool that helps you build strong, accurate proofs. It's like having a helpful assistant who makes sure your logical thinking is top-notch.

3. COQ-SHELL

Imagine Coq-Shell as a magical text box where you can type in math problems and proofs. It's like having a super smart calculator that not only gives you answers but also checks if your thinking is correct.

Here's how it works:

Typing: 

You type in your math problems and proofs using special commands.

Checking: 

Coq-Shell checks your work step-by-step to make sure it's logically sound.

Feedback: 

It gives you feedback, like if you made a mistake or if your proof is correct.

So, Coq-Shell is a tool that helps you explore math and logic in a fun and interactive way. It's like having a math wizard by your side, guiding you through your calculations and helping you discover new things!

4. CONCLUSION

In this tutorial, you have received a brief overview of Coq, Coq-IDE, and Coq-Shell.

5. REFERENCES

Bird, R. (2015). Thinking Functionally with Haskell. Cambridge, England: Cambridge University Press.

Davie, A. (1992). Introduction to Functional Programming Systems Using Haskell. Cambridge, England: Cambridge University Press.

Goerzen, J. & O'Sullivan, B. &  Stewart, D. (2008). Real World Haskell. Sebastopol, CA: O'Reilly Media, Inc.

Hutton, G. (2007). Programming in Haskell. New York: Cambridge University Press.

Lipovača, M. (2011). Learn You a Haskell for Great Good!: A Beginner's Guide. San Francisco, CA: No Starch Press, Inc.

Thompson, S. (2011). The Craft of Functional Programming. Edinburgh Gate, Harlow, England: Pearson Education Limited.

HASKELL TO AGDA AND COQ

 

REVISED: Thursday, October 31, 2024

1. INTRODUCTION

As software systems become more complex and critical, the demand for rigorous verification methods will grow. Agda and Coq, with their ability to formally prove the correctness of programs, are well-positioned to play a significant role in this domain.

These languages are excellent tools for teaching and research in computer science and mathematics. They provide a solid foundation for understanding complex concepts and developing formal reasoning skills.

Agda and Coq's strengths in expressing complex specifications and proofs make them suitable for specialized domains such as cryptography, security, and systems programming.

There's potential for integrating ideas from dependent type theory into mainstream programming languages. This could lead to more reliable and secure software development practices.

2. OVERVIEW

Agda:

Dependent Types: Agda allows you to define types that depend on values, making it possible to express complex relationships between data and functions.

Proofs as Programs: In Agda, proofs are written as programs, and programs are verified proofs. This principle, known as the Curry-Howard isomorphism, enables you to write code that is both correct and formally verified.

Interactive Development: Agda provides an interactive development environment where you can define functions, prove theorems, and experiment with different approaches.

Coq:

Coq is French for Rooster. Coq is free, open-source software.

Coq is an interactive theorem prover, development started in 1983 and was first released in 1989.

Implemented in the OCaml programming language.

Reference Manual  https://coq.inria.fr/doc/V8.20.0/refman/

Calculus of Inductive Constructions: Coq is based on a powerful type theory called the Calculus of Inductive Constructions, which allows for higher-order reasoning and the definition of complex mathematical structures.

Tactics: Coq uses tactics to guide the proof process, allowing you to break down complex proofs into smaller, more manageable steps.

Formal Verification: Coq is widely used for formal verification of software and hardware, ensuring that systems are correct by construction.

3. Learning Resources:

Agda:

Official Tutorial:

https://agda.readthedocs.io/en/v2.6.0.1/getting-started/tutorial-list.html

Software Foundations in Agda:

 https://softwarefoundations.cis.upenn.edu/

Type-Driven Development with Idris:

https://www.amazon.com/Type-driven-Development-Idris-Edwin-Brady/dp/1617293024 (While this book is about Idris, it covers many concepts relevant to Agda)

Coq:

Software Foundations: 

The Coq system contains the functional programming language Gallina.

https://softwarefoundations.cis.upenn.edu/

https://www.youtube.com/watch?v=BGg-gxhsV4E&list=PLre5AT9JnKShFK9l9HYzkZugkJSsXioFs

Certified Programming with Coq:

https://www.amazon.com/Certified-Programming-Dependent-Types-Introduction/dp/0262026651

Coq'Art: The Art of Proof and Programming: 

https://link.springer.com/book/10.1007/978-3-662-07964-5

4. Getting Started:

Install: Download and install Agda or Coq for your operating system.

Learn the Basics: Start with the official tutorials or books to understand the syntax and basic concepts.

Practice: Work through exercises and examples to gain practical experience.

Explore Libraries: Use existing libraries to learn from others and build upon their work.

Join the Community: Participate in online forums and communities to ask questions and get help.

Remember, learning Agda and Coq requires patience and persistence. Don't be afraid to experiment and make mistakes. The more you practice, the better you'll become.

3. CONCLUSION

While Agda and Coq may not become mainstream programming languages like Python or JavaScript, their impact on the software development landscape is likely to grow. As the demand for rigorous verification and formal methods increases, these languages have the potential to become indispensable tools for developers and researchers alike.

4. REFERENCES

Bird, R. (2015). Thinking Functionally with Haskell. Cambridge, England: Cambridge University Press.

Davie, A. (1992). Introduction to Functional Programming Systems Using Haskell. Cambridge, England: Cambridge University Press.

Goerzen, J. & O'Sullivan, B. &  Stewart, D. (2008). Real World Haskell. Sebastopol, CA: O'Reilly Media, Inc.

Hutton, G. (2007). Programming in Haskell. New York: Cambridge University Press.

Lipovača, M. (2011). Learn You a Haskell for Great Good!: A Beginner's Guide. San Francisco, CA: No Starch Press, Inc.

Thompson, S. (2011). The Craft of Functional Programming. Edinburgh Gate, Harlow, England: Pearson Education Limited.

HASKELL DIRECT PROOF

REVISED: Monday, October 28, 2024

1. INTRODUCTION

A Direct Proof is a mathematical method that uses known facts to show the truth or falsehood of a statement. It's a sequence of statements that use definitions, theorems, and logic to prove a conclusion. 

If P then Q or P implies Q is a Direct Proof. For our Direct Proof, we assume P is True and accomplish the proof by using P to prove Q is True. 

An expression of the form P => Q (if P, then Q; Q if P) is called the implication of P and Q. P is the antecedent of the implication and Q the consequent.

If we want to implement implication in Haskell, we can do so in terms of if, then, not, and || or.

The Boolean otherwise is defined as the value True.

The only time an implication is False is when the antecedent P is True and the consequent Q is False.

2. DEFINITIONS (DEF)

DEF 1

An integer 'n' is even if and only if there exists an integer 'k' such that n = 2k

 

DEF 2

An integer 'n' is odd if and only if there exists an integer 'k' such that n = 2k+ 1

DEF 3

Two integers 'a' and 'b' are consecutive if and only if  b = a + 1

3. PROOF 1

Theorem: The sum of any two consecutive integers is odd.

Assume 'a' and 'b' are consecutive integers.

b = a + 1                                                              -- def 3

If 'a' and 'b' are consecutive integers, then by Definition 3, 'b' must be one more than 'a'.

(a + b) = a + (a + 1)                                             -- def 3

(a + b) = 2a + 1                                                    -- def 2

Since 2a is an even integer (by Definition 1), and adding 1 to an even integer always results in an odd integer (by Definition 2), (a + b) is odd.

Q.E.D. “Which was to be demonstrated".  Signifies the end of a proof.

A  □ tombstone symbol is also often used to signify the end of a proof.

4. PROOF 2

While Haskell can be used to represent and reason about mathematical proofs, it's not a direct tool for automating the process of constructing complex proofs. However, we can leverage its type system and functional paradigm to encode simple proofs and reason about them.

A Simple Proof in Haskell: The Sum of Two Even Numbers

Let's consider a simple proof: "The sum of two even numbers is even." We can represent this in Haskell using types and functions:

Theorem: The sum of two even numbers is even.

Haskell

-- Define an even number as a number divisible by 2

data Even = Even Int

-- Define a function to add two even numbers

addEven :: Even -> Even -> Even

addEven (Even x) (Even y) = Even (x + y)

Breakdown:

Data Type Even:

This data type represents an even number. It takes an integer and wraps it in the Even constructor.

Function addEven:

This function takes two Even values and returns an Even value.

It extracts the underlying integers, adds them, and constructs a new Even value.

How Does This Represent a Proof?

Type Safety: The type system ensures that the addEven function can only be applied to two Even values. This guarantees that the input numbers are indeed even.

Functional Purity: Haskell's functional nature ensures that the addEven function always produces the same output for the same input. This eliminates side effects and makes reasoning about the function's behavior straightforward.

Limitations and Advanced Techniques:

While this simple example demonstrates the potential of Haskell for representing and reasoning about mathematical proofs, it's important to note its limitations:

Complex Proofs: For more complex proofs involving multiple steps, quantifiers, and logical connectives, Haskell's type system alone may not be sufficient.

Proof Automation: While Haskell can help formalize and reason about proofs, it doesn't automate the discovery of proofs. Human ingenuity is still required to devise proof strategies.

Advanced Techniques:

Dependent Types: Dependent types allow types to depend on values, enabling more expressive and precise type systems. This can be used to encode more complex mathematical properties.

Proof Assistants: Tools like Agda and Coq are built on top of dependent type theories and provide formal proof systems for verifying mathematical theorems.

5. CONCLUSION

While Haskell is a powerful tool for representing and reasoning about mathematical concepts, it's not a substitute for human mathematical reasoning. However, it can be used to formalize and verify proofs, especially in conjunction with advanced techniques like dependent types and proof assistants.

The goal of a proof is not only to arrive at the correct conclusion but also to present a clear and convincing argument. You want to make your proofs rigorous and easy to understand.

6. REFERENCES

Bird, R. (2015). Thinking Functionally with Haskell. Cambridge, England: Cambridge University Press.

Davie, A. (1992). Introduction to Functional Programming Systems Using Haskell. Cambridge, England: Cambridge University Press.

Goerzen, J. & O'Sullivan, B. &  Stewart, D. (2008). Real World Haskell. Sebastopol, CA: O'Reilly Media, Inc.

Hutton, G. (2007). Programming in Haskell. New York: Cambridge University Press.

Lipovača, M. (2011). Learn You a Haskell for Great Good!: A Beginner's Guide. San Francisco, CA: No Starch Press, Inc.

Thompson, S. (2011). The Craft of Functional Programming. Edinburgh Gate, Harlow, England: Pearson Education Limited.

HASKELL FUNCTION PROOFS

 

REVISED: Monday, October 28, 2024

1. INTRODUCTION

Haskell Functions as Mathematical Functions

In Haskell, functions are conceptualized as mathematical functions, mapping inputs to outputs. This means they take one or more values as arguments and produce a single result.

Pure Functions

Haskell functions are inherently pure, meaning they have the following properties:

No side effects: They don't modify external state or produce observable effects beyond their return value.

Referential transparency: Replacing a function call with its result doesn't change the program's behavior.

First-Class Citizens

Functions in Haskell are first-class citizens, treated like any other data type:

Passed as arguments: You can pass functions as arguments to other functions.

Returned as values: Functions can return other functions as results.

Assigned to variables: You can store functions in variables.

Syntax and Types

Definition: Functions are defined using the = operator.

Type annotation: The type of a function is specified after its name, using ::. For example, f :: Int -> Int indicates that f takes an integer as input and returns an integer.

Arguments: Multiple arguments are separated by spaces.

Return value: The return value is the expression on the right side of the = operator.

Examples

Simple function:

add :: Num a => a -> a -> a

add x y = x + y

Function taking multiple arguments:

multiply :: Num a => a -> a -> a -> a

multiply x y z = x * y * z

Function returning a function:

makeAdder :: Num a => a -> a -> a

makeAdder x = (\y -> x + y)

Higher-Order Functions

Haskell supports higher-order functions, taking functions as arguments or returning functions as results. This enables powerful programming techniques like:

Map: Applies a function to each element of a list.

map :: (a -> b) -> [a] -> [b]

Filter: Selects elements from a list based on a predicate function.

filter :: (a -> Bool) -> [a] -> [a]

Reduce: Combines elements of a list using a binary function.

reduce :: Integral a => a -> a -> Ratio a

Recursion

Recursion is a common programming technique in Haskell, where a function calls itself to solve smaller instances of a problem. Haskell's type system and pattern matching make it well-suited for recursive functions.

Benefits of Haskell Functions

Readability: Haskell's functional style and concise syntax make code more readable and easier to understand.

Correctness: Pure functions are easier to reason about and test for correctness.

Concurrency: Haskell's functional nature makes it well-suited for concurrent programming.

Modularity: Functions can be composed to build complex programs from smaller, reusable components.

By understanding these concepts, you can effectively use Haskell functions to write elegant, efficient, and maintainable code.

2. PROOFS

Computer program function proofs are mathematical proofs partially or fully generated by a computer program.

You can evaluate (prove) Integer arithmetic; however, computers still have problems with Floating-Point arithmetic. 

Before assuming a Lemma check it with QuickCheck. 

A function algorithm proof is a step-by-step procedure or formula for calculations, problem-solving operations, or accomplishing a task in a certain number of steps.

There are four basic proof techniques used in mathematics: Direct Proof, Proof by Contradiction, Proof by Induction, and Proof by Contrapositive.

PROOF BY INDUCTION EXAMPLE

Proving a recursion reverse function:

sum (reverse [])       = sum []                                               -- def reverse base case

sum (reverse (x:xs)) = sum (reverse xs ++ [x])                  -- def reverse recursion

Base Case:

sum (reverse []) = sum []

This follows directly from the definition of reverse and sum.

Recursive Case:

Inductive Hypothesis: Assume that sum (reverse ys) = sum ys for all lists ys.

Inductive Steps:

sum (reverse (x:xs)) = sum (reverse xs ++ [x])       -- definition of `reverse`

sum (reverse (x:xs)) = sum (reverse xs) + sum [x]  -- lemma (proven below separately)

sum (reverse (x:xs)) = sum xs + sum [x]                  -- inductive hypothesis

sum (reverse (x:xs)) = sum xs + x                             -- definition of `sum`

sum (reverse (x:xs)) = sum (x:xs)                             -- definition of `sum`

Key Points:

The proof relies on a strong inductive hypothesis and a correctly proven lemma.

The commutativity of sum is implicitly used, a direct consequence of the definition.

A formal proof of the lemma enhances the rigor of the overall proof.

LEMMA PROOF

The lemma can be proven using the definition of sum and induction on the length of xs.

Proving the Lemma: sum (reverse xs ++ [x]) = sum (reverse xs) + sum [x]

Proof by Induction on the Length of xs:

Base Case:

When xs = []:

sum (reverse [] ++ [x]) = sum ([x]) = x

sum (reverse []) + sum [x] = sum [] + sum [x] = 0 + x = x

Thus, the equation holds for the base case.

Recursive Case:

Inductive Hypothesis: Assume the equation holds for a list xs of length n. That is:

sum (reverse xs ++ [x]) = sum (reverse xs) + sum [x]

Inductive Steps:

Consider a list (y:xs) of length n+1:

sum (reverse (y:xs) ++ [x])

= sum (reverse xs ++ [y] ++ [x])          -- Definition of `reverse`

= sum (reverse xs ++ [y + x])               -- Definition of `++` and `sum`

= sum (reverse xs) + sum [y + x]          -- Inductive Hypothesis

= sum (reverse xs) + (y + x)                   -- Definition of `sum`

= (sum (reverse xs) + y) + x                   -- Associativity of `+`

= (sum (reverse xs) + sum [y]) + x         -- Definition of `sum`

= sum (reverse xs) + (sum [y] + x)         -- Associativity of `+`

= sum (reverse xs) + sum [y, x]               -- Definition of `sum` and `++`

= sum (reverse xs) + sum [x, y]               -- Commutativity of `+`

= sum (reverse xs) + sum [x] + sum [y]  -- Definition of `sum`

= sum (reverse xs) + sum [x]                    -- Definition of `sum` for a singleton list

Therefore, by the principle of mathematical induction, the lemma holds for all lists xs.

3. CONCLUSION

The concept of pure functionality in Haskell makes its code easier to prove correct than imperative languages.

4. REFERENCES

Bird, R. (2015). Thinking Functionally with Haskell. Cambridge, England: Cambridge University Press.

Davie, A. (1992). Introduction to Functional Programming Systems Using Haskell. Cambridge, England: Cambridge University Press.

Goerzen, J. & O'Sullivan, B. &  Stewart, D. (2008). Real World Haskell. Sebastopol, CA: O'Reilly Media, Inc.

Hutton, G. (2007). Programming in Haskell. New York: Cambridge University Press.

Lipovača, M. (2011). Learn You a Haskell for Great Good!: A Beginner's Guide. San Francisco, CA: No Starch Press, Inc.

Thompson, S. (2011). The Craft of Functional Programming. Edinburgh Gate, Harlow, England: Pearson Education Limited.