Tag : computer science

Most physical systems are modelized using continuous mathematics. A cellular automaton is different : it is a discrete system. A regular grid of cells in one, two or several dimensions is the stage where the dynamics is taking place. Each cell can have a finite number of states. The state of a cell is changing as a function of a time which is also discrete.

Before continuing my exploration of the specification and extraction of softwares in Coq, I think I should make a pause and focus a little on Coq basics like the differences between Set and Prop and the meaning of a type like 4>0 ...

One month ago I did not know a lot about logic : just truth tables for some connectives. But, for some time I have been having fun with Haskell and it finally convinced me to use some of my spare time to learn about logic. Of course, you can code in Haskell without knowing a lot about logic, the Curry-Howard isomorphism and all that but it is much more fun to code in Haskell if you know a bit about it. So, thanks to my Christmas vacations, and the fact that being French I have long vacations :-), I read a few papers about logic : classical, intuitionistic, modal, linear etc... This post is an attempt to summarize what I think I have understood and I hope it may be useful to other newbies too.