Types and trace effects of higher order programs

DOI10.1017/S0956796807006466zbMATH Open1142.68020OpenAlexW2163672449MaRDI QIDQ5451968FDOQ5451968

Scott F. Smith, David van Horn, Christian Skalka

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)

Cites Work

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

Cited In (9)

• Regular and context-free nominal traces
• Formalizing Soundness of Contextual Effects
• Safe Adaptation Through Implicit Effect Coercion
• Nominal Automata for Resource Usage Control
• Temporal refinements for guarded recursive types
• Systematic abstraction of abstract machines
• Automated temporal verification for algebraic effects
• Types and trace effects for object orientation
• Enforcing Programming Guidelines with Region Types and Effects

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)