On the Versatility of Open Logical Relations

DOI10.1007/978-3-030-44914-8_3OpenAlexW3023853936MaRDI QIDQ5041087

Ugo Dal Lago, Gilles Barthe, Francesco Gavazzo, Raphaëlle Crubillé

Publication date: 13 October 2022

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2002.08489

zbMATH Keywords

automatic differentiationlambda calculuslogical relationscontinuity analysis

Mathematics Subject Classification ID

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

Related Items (8)

Differential logical relations. II: Increments and derivatives ⋮ Smart Choices and the Selection Monad ⋮ CHAD for expressive total languages ⋮ Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library ⋮ Correctness of automatic differentiation via diffeologies and categorical gluing ⋮ Densities of almost surely terminating probabilistic programs are differentiable almost everywhere ⋮ Reverse AD at higher types: pure, principled and denotationally correct ⋮ Unnamed Item

Uses Software

• DiffSharp

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Operational domain theory and topology of sequential programming languages
• Nesting forward-mode AD in a functional framework
• Automatic differentiation of algorithms
• Correctness of automatic differentiation via diffeologies and categorical gluing
• A Kripke logical relation for effect-based program transformations
• Syntactic Logical Relations for Polymorphic and Recursive Types
• Logical relations for fine-grained concurrency
• Step-Indexed Logical Relations for Probability
• Noninterference for free
• The impact of higher-order state and control effects on local relational reasoning
• A very modal model of a modern, major, general type system
• Lazy multivariate higher-order forward-mode AD
• Evaluating Derivatives
• Categories for Types
• Semantics for probabilistic programming
• Higher-Order Interpretations and Program Complexity
• Domain theory and differential calculus (functions of one variable)
• A new Characterization of Type-2 Feasibility
• A Language for Differentiable Functions
• Continuity analysis of programs
• Logical Relations and Nondeterminism
• Abstract effects and proof-relevant logical relations
• Intensional interpretations of functionals of finite type I
• Programming Languages and Systems

This page was built for publication: On the Versatility of Open Logical Relations