Types and trace effects of higher order programs

DOI10.1017/S0956796807006466MaRDI QIDQ5451968zbMATH OpenOpenAlexFDO

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 \)-calculusautomatically verifiable program logicsmodel-checking techniques

Mathematics Subject Classification ID

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

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

(13)

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

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)