Ph: 416-736-2100, ext. 77844, Fax 416-736-5924,
e-mail: peter at cse.yorku.ca
CSE 3341 .03 M Introduction to Program Verification.
Chapters 0-3
Chapters 4-6
Chapters 7-9
some source code and binaries are available at ftp://cse.yorku.ca/cs/dept/ftp/pub/peter/SVT/
GNU Prolog stand-alones
SWI Prolog stand-alones
These programs and their sources (excluding portions copyrighted by others) are made available under a Creative Commons License which requires attribution, permits reproduction, distribution and derivative works (as long as the derivative works are licensed under the same terms as the originals), and prohibits unauthorized commercial use.
"The Intercom Ontario Field Trial: Lessons Learned", (with D. Thomassin Singh, J. Durlak, and D. De Shane-Gill), Canadian Journal of Communications, 24 (3), 1999.
"Intercom Ontario: a residential multimedia distribution system in operation", with T. Jurenka, Multimedia to the Home, Bandwidth Battles, Saskatoon, August, 1997.
"A Field Trial of Residential Multimedia Services", with J. Durlak,
Conference on Multimedia to the Home, The Emerging On-Ramps, Saskatoon,
August, 1995.
Presents fundamental results on the application of lattice theory to mereology, information flow among parts of a system, and the duality of transmission and control.
Chapter I - Introduction
Chapter II - Decompositions
Chapter III - Localization of Information
Chapter IV - Basic Structure of a Computer and the Concept of Control
Chapter V - Ranges and Domains of Instructions; Prediction and Transmission
Chapter VI - Access, Access Structures, and the Concept of Stored Program
Appendices, List of Symbols, List of References
"The algebra of distributionally defined classes", Cahiers de linguistique theorique et applique, 10, Fasc. 1, 1973.
Intended in some ways as an "homage" to Rulon Wells and immediate constituent analysis, which had become, perhaps undeservedly, a dead-end in linguistic research with the rise of transformational grammar.
Metaphysical lattices (Powerpoint)
Intention and backward-chaining in Plato's Philebus
From Behavior to Structure: construction of a minimal specification of internal causal structure (state-transition function) from a specification of external behavior (I/O mapping) for a very general class of finite or infinite transducers, using the lattice of behavioral congruences. (A reworking of the Myhill-Nerode and Scott-Rabin theorems in very general terms.)
"Liddle Alice"
Last Updated: December 10, 2009