Lightweight Static Capabilities

DOI10.1016/j.entcs.2006.10.039zbMath1277.68052OpenAlexW2098252947MaRDI QIDQ2866337

Chung-Chieh Shan, Oleg Kiselyov

Publication date: 13 December 2013

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2006.10.039

zbMATH Keywords

verificationmodular programmingsafety propertystatic types

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

\textsc{Mnemonics}: type-safe bytecode generation at run time

Uses Software

• Haskell
• OCaml
• LCF
• TALx86

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Singleton, union, and intersection types for program extraction
• Types for modules
• Transparent modules with fully syntatic signatures
• A type system for higher-order modules
• Tagless staged interpreters for typed languages
• Faking it Simulating dependent types in Haskell
• Monadic encapsulation of effects: a revised approach (extended version)
• Phantom types and subtyping
• A Substructural Type System for Delimited Continuations
• Do we need dependent types?
• Deciding type equivalence in a language with singleton kinds
• A bisimulation for type abstraction and recursion