Types and trace effects of higher order programs

DOI10.1017/S0956796807006466zbMath1142.68020OpenAlexW2163672449MaRDI QIDQ5451968

Scott F. Smith, David A. Vanhorn, 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

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

Related Items (9)

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

Uses Software

• Bebop
• MOPS

Cites Work

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

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