Date of Award




Document Type

Master's Thesis

Degree Name

Master of Science (MS)


Department of Computer Science

Content Description

1 online resource (iv, 31 pages)

Dissertation/Thesis Chair

Paliath Narendran

Committee Members

Paliath Narendran


concurrency, concurrent SML, Curry Howard, natural deduction, pi calculus, programming language, Programming languages (Electronic computers), Computer multitasking, Computer logic, Logic, Symbolic and mathematical

Subject Categories

Computer Sciences


In order to fully utilize the potential of current architectures, programmers must program withconcurrency in mind. Concurrent processes can be extremely challenging to reason about due tounexpected program behavior that may emerge from interaction between processes. One approachto deal with this difficulty is to study new programming languages that offer an abstraction forconcurrency. This thesis focuses on developing a logical interpretation for concurrent processesand incorporating it in an existing functional programming language called SML. We developthis feature upon the fact that a proof of a theorem in logic can be expressed as a program in aprogramming language. This relation allows us to design a formal system that behaves both as aproof system and a typed programming language.We introduce a system of Natural Deduction to develop a logical basis for concurrent program-ming. This works as a proof system in which logic is defined by inference rules and its propositionscan be seen as resource combinators that keep on changing throughout the derivation which leadsto the idea of using Natural Deduction as a logic of concurrent computation. Lastly, we constructa concurrent programming language called concurrent SML by assigning a syntactical form to thelogical foundation established through natural deduction relations and integrating it with a func-tional programming language.