Towards proving type safety of .NET CIL

DOI10.1016/j.scico.2008.05.004zbMath1154.68359OpenAlexW2072260485MaRDI QIDQ941469

Nicu G. Fruja

Publication date: 1 September 2008

Published in: Science of Computer Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.scico.2008.05.004

zbMATH Keywords

operational semanticssecurityvirtual machinestype safetybytecode verification.NETCILCLR

Mathematics Subject Classification ID

Theory of operating systems (68N25)

Related Items (3)

The Subject-Oriented Approach to Software Design and the Abstract State Machines Method ⋮ Towards proving type safety of .NET CIL ⋮ Towards proving type safety of \(\mathrm{C}^{\#}\)

Uses Software

• ML
• LPTP
• AsmL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A high-level modular definition of the semantics of C\(_{\sharp}\)
• Towards proving type safety of .NET CIL
• A theory of type polymorphism in programming
• A mathematical definition of full Prolog
• Formal specification and verification of the C\(\#\) thread model
• The theoretical foundations of LPTP (a logic program theorem prover)
• Abstract State Machines
• Evolving Algebras 1993: Lipari Guide
• Formal Methods for Components and Objects
• Programming Languages and Systems
• Abstract State Machines 2004. Advances in Theory and Practice

This page was built for publication: Towards proving type safety of .NET CIL