Types and trace effects of higher order programs

DOI10.1017/S0956796807006466MaRDI QIDQ5451968zbMATHOpenAlexFDO

Authors Christian Skalka, Scott F. Smith, David van Horn

Publication date 27 March 2008

Published in Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/s0956796807006466

zbMATH Keywords

\(\lambda \)-calculusmodel-checking techniquesautomatically verifiable program logics

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Functional programming and lambda calculus (68N18)

Recommendations

• Programming Languages and Systems
• Model checking higher-order programs
• Types and trace effects for object orientation
• Model-checking higher-order programs with recursive types
• Types and higher-order recursion schemes for verification of higher-order programs

Cites work

• A lattice-theoretical fixpoint theorem and its applications
• Results on the propositional \(\mu\)-calculus

Cited in

(12)

• Temporal refinements for guarded recursive types
• Higher-order program verification and language-based security (extended abstract)
• Types and trace effects for object orientation
• Nominal automata for resource usage control
• Safe adaptation through implicit effect coercion
• Enforcing Programming Guidelines with Region Types and Effects
• Automated temporal verification for algebraic effects
• Roles, stacks, histories: A triple for Hoare
• Systematic abstraction of abstract machines
• Regular and context-free nominal traces
• Programming Languages and Systems
• Formalizing Soundness of Contextual Effects

Describes a project that uses

Uses Software

• Bebop
• MOPS

This page was built for publication: Types and trace effects of higher order programs

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