Lightweight static capabilities

DOI10.1016/J.ENTCS.2006.10.039MaRDI QIDQ2866337zbMATH OpenOpenAlexFDO

Authors Oleg Kiselyov, Chung-Chieh Shan

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

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

Recommendations

• scientific article; zbMATH DE number 2163037
• Secure distributed programming with value-dependent types
• Secure distributed programming with value-dependent types
• Gradual program verification
• Modular verification of programs with effects and effects handlers

Cites work

• scientific article; zbMATH DE number 1692889 (Why is no real title available?)
• scientific article; zbMATH DE number 3902022 (Why is no real title available?)
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 65535 (Why is no real title available?)
• scientific article; zbMATH DE number 1531624 (Why is no real title available?)
• scientific article; zbMATH DE number 1759364 (Why is no real title available?)
• A Substructural Type System for Delimited Continuations
• A bisimulation for type abstraction and recursion
• A type system for higher-order modules
• Deciding type equivalence in a language with singleton kinds
• Do we need dependent types?
• Faking it Simulating dependent types in Haskell
• Monadic encapsulation of effects: a revised approach (extended version)
• Phantom types and subtyping
• Singleton, union, and intersection types for program extraction
• Tagless staged interpreters for typed languages
• Transparent modules with fully syntatic signatures
• Types for modules

Cited in

(1)

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

Describes a project that uses

Uses Software

• TALx86
• LCF
• OCaml
• Haskell

This page was built for publication: Lightweight static capabilities

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2866337)