| ชื่อเรื่อง | : | The Polymorphic Pi-Calculus: Theory and Implementation |
| นักวิจัย | : | Turner , David |
| คำค้น | : | - |
| หน่วยงาน | : | Edinburgh Research Archive, United Kingdom |
| ผู้ร่วมงาน | : | Milner, Robert , Engineering and Physical Sciences Research Council (EPSRC) |
| ปีพิมพ์ | : | 2539 |
| อ้างอิง | : | http://hdl.handle.net/1842/395 |
| ที่มา | : | - |
| ความเชี่ยวชาญ | : | - |
| ความสัมพันธ์ | : | - |
| ขอบเขตของเนื้อหา | : | - |
| บทคัดย่อ/คำอธิบาย | : | We investigate whether the Pi-calculus is able to serve as a good foundation for the design and implementation of a strongly-typed concurrent programming language. The first half of the dissertation examines whether the Pi-calculus supports a simple type system which is flexible enough to provide a suitable foundation for the type system of a concurrent programming language. The second half of the dissertation considers how to implement the Pi-calculus efficiently, starting with an abstract machine for Pi-calculus and finally presenting a compilation of Pi-calculus to C. We start the dissertation by presenting a simple, structural type system for Pi-calculus, and then, after proving the soundness of our type system, show how to infer principal types for Pi-terms. This simple type system can be extended to include useful type-theoretic constructions such as recursive types and higher-order polymorphism. Higher-order polymorphism is important, since it gives us the ability to implement abstract datatypes in a type-safe manner, thereby providing a greater degree of modularity for Pi-calculus programs. The functional computational paradigm plays an important part in many programming languages. It is well-known that the Pi-calculus can encode functional computation. We go further and show that the type structure of lambda-terms is preserved by such encodings, in the sense that we can relate the type of a lambda-term to the type of its encoding in the Pi-calculus. This means that a Pi-calculus programming language can genuinely support typed functional programming as a special case. An efficient implementation of Pi-calculus is necessary if we wish to consider Pi-calculus as an operational foundation for concurrent programming. We first give a simple abstract machine for Pi-calculus and prove it correct. We then show how this abstract machine inspires a simple, but efficient, compilation of Pi-calculus to C (which now forms the basis of the Pict programming language implementation). |
| บรรณานุกรม | : |
Turner , David . (2539). The Polymorphic Pi-Calculus: Theory and Implementation.
กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom . Turner , David . 2539. "The Polymorphic Pi-Calculus: Theory and Implementation".
กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom . Turner , David . "The Polymorphic Pi-Calculus: Theory and Implementation."
กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom , 2539. Print. Turner , David . The Polymorphic Pi-Calculus: Theory and Implementation. กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom ; 2539.
|
