Two-level semantics and abstract interpretation

DOI10.1016/0304-3975(89)90091-1zbMath0696.68093OpenAlexW1981580304MaRDI QIDQ911319

Flemming Nielson

Publication date: 1989

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(89)90091-1

zbMATH Keywords

abstract interpretation theorycompile-time data typesrun-time data typesScott-Strachey denotational semantics

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) General topics in the theory of software (68N01) Theory of software (68N99)

Related Items

Representing Control: a Study of the CPS Transformation, Precise goal-independent abstract interpretation of constraint logic programs., Sound Bit-Precise Numerical Domains, On-line and off-line partial evaluation: semantic specifications and correctness proofs, Proving the correctness of compiler optimisations based on a global analysis: a study of strictness analysis^†, Program verification: state of the art, problems, and results. I, A security flow control algorithm and its denotational semantics correctness proof, Using transformations in the implementation of higher-order functions, The reduced relative power operation on abstract domains, A new abstraction framework for affine transformers, Representing Control: a Study of the CPS Transformation, MetaML and multi-stage programming with explicit annotations, Extracting Program Logics From Abstract Interpretations Defined by Logical Relations, Kleene's Logic with equality, Semantics-directed program analysis: A tool-maker's perspective

Cites Work

• The tensor product of continuous lattices
• Strictness analysis for higher-order functions
• Category theory and computer programming. Tutorial and Workshop, Guildford, U.K., September 16-20, 1985. Proceedings
• Two-level semantics and code generation
• Automatic binding time analysis for a typed \(\lambda\)-calculus
• Control Flow Aspects of Semantics-Directed Compiling
• Program transformations in a denotational setting
• On the power of list iteration
• Algebraic specification of data types: A synthetic approach
• Deriving Target Code as a Representation of Continuation Semantics
• The Category-Theoretic Solution of Recursive Domain Equations
• The λ-calculus is ω-incomplete
• Data Types as Lattices
• A Powerdomain Construction
• Can programming be liberated from the von Neumann style?
• A general purpose macrogenerator
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item