Programming Languages and Systems

DOI10.1007/11693024MaRDI QIDQ5899009zbMATH OpenOpenAlexFDO

Authors Amal Ahmed

Publication date 2 May 2007

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11693024

Mathematics Subject Classification ID

Logic in computer science (03B70) Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Syntactic logical relations for polymorphic and recursive types
• Transfinite step-indexing: decoupling concrete and logical steps
• Relational Reasoning for Recursive Types and References
• Step-indexed logical relations for probability
• scientific article; zbMATH DE number 1342222

Cited in

(39)

• A family of syntactic logical relations for the semantics of Haskell-like languages
• Proving correctness of a compiler using step-indexed logical relations
• Translation certification for smart contracts
• Temporal refinements for guarded recursive types
• Observational program calculi and the correctness of translations
• Selective strictness and parametricity in structural operational semantics, inequationally
• A Kripke logical relation for effect-based program transformations
• Differential logical relations. II: Increments and derivatives
• Program equivalence in an untyped, call-by-value functional language with uncurried functions
• Transfinite step-indexing: decoupling concrete and logical steps
• A higher-order abstract syntax approach to verified transformations on functional programs
• Syntactic logical relations for polymorphic and recursive types
• Step-indexed logical relations for probability
• A Complete, Co-inductive Syntactic Theory of Sequential Control and State
• A Step-indexed Semantics of Imperative Objects
• A relational realizability model for higher-order stateful ADTs
• Logical relations for coherence of effect subtyping
• Gradual type theory
• Relational cost analysis in a functional-imperative setting
• Taming the merge operator
• On the versatility of open logical relations. Continuity, automatic differentiation, and a containment theorem
• scientific article; zbMATH DE number 7407781 (Why is no real title available?)
• A case study in programming coinductive proofs: Howe's method
• Free theorems and runtime type representations
• Relational Reasoning for Recursive Types and References
• scientific article; zbMATH DE number 7324347 (Why is no real title available?)
• A type-directed, dictionary-passing translation of method overloading and structural subtyping in Featherweight Generic Go
• Semantic preservation for a type directed translation scheme of Featherweight Go
• Polarized subtyping
• A Dictionary-Passing Translation of Featherweight Go
• Existential types for relaxed noninterference
• A fibrational tale of operational logical relations: pure, effectful and differential
• Logical predicates in higher-order mathematical operational semantics
• Call-by-value and call-by-name: a simple proof of a classic theorem
• Bialgebraic reasoning on higher-order program equivalence
• A logical approach to type soundness
• Automatic differentiation for ML-family languages: correctness via logical relations
• A verified framework for higher-order uncurrying optimizations
• Typing termination in a higher-order concurrent imperative language

This page was built for publication: Programming Languages and Systems

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