Tomáš Petříček, 309 (3rd floor)
petricek@d3s.mff.cuni.cz
https://tomasp.net | @tomaspetricek
Lectures: Monday 12:20, S7
https://d3s.mff.cuni.cz/teaching/nprg075
ENIAC programmed by plugging wires and flipping switches
"The ENIAC was a son-of-a-bitch to program" - Jean (Jennings) Bartik
In a mathematical science, it is possible to deduce from the basic assumptions, the important properties of the entities treated by the science.
Syntax and semantics of trivial Algol subset
\(micro(\pi,\xi)\) gives the final state of a program \(\pi\) run in a state \(\xi\)
"Description of the state of an Algol computation will clarify (..) compiler design"
Operational semantics
and type system for a complete language
Even language this simple had murky parts!
// Function: 'a -> 'a list
let callLogger =
// List: 'a list
let mutable log = []
fun x ->
log <- x :: log
log
// Can we call this with:
callLogger 10
callLogger "hi"
ML makes top-level definitions polymorphic
Allowing that for values is unsound!
Easier to write than axiomatic or denotational
But harder to use for program equivalence
Good textbook and popular in PL research community
Works for programs that do not terminate
followMouseAndDelay u =
follow `over` later 1 follow
where
follow = move (mouseMotion u) jake
mouseMotion
represents current mouse positionlater
delays time by X secondsover
overlays multiple animationsEvents represented by Observable<T>
Produces values when something happen
Operators turn one or more observables into a new one
Useful design guide and for making formal claims
Explains core ideas of a system in a succinct way
The danger is producing languages that look
well on paper!
null
dereferencing with typesFormal models of programming
Tomáš Petříček, 309 (3rd floor)
petricek@d3s.mff.cuni.cz
https://tomasp.net | @tomaspetricek
https://d3s.mff.cuni.cz/teaching/nprg075
Semantics
History
Reactive
Calculi