MODELS AND METAMODELS FOR SOFTWARE VERIFICATION AND VALIDATION
A brief introduction to l-calculus Main issues Recursive functions Computing on data types Functional programming A brief introduction to typed l-calculi What are types, what do/can they denote/represent Curry - Howard - Martin-Löf - De Bruijn analogy Computational contents of proofs 1 Computational contents of proofs 2 Processes A brief introduction to p-calculi The surprising expressive power of p-calculus p-calculus: syntax p-calculus: reduction semantics p-calculus: structural congruence p-calculus: labelled transition system Omologies between l and p Mobile communications 1 Mobile communications 2 Mobile communications 3 Private channel passing (scope extrusion) 1 Private channel passing (scope extrusion) 2 Private channel passing (scope extrusion) 3 Example: ftp 1 Example: ftp 2 Example: ftp 3
