Ott: Effective tool support for the working semanticist

DOI10.1017/S0956796809990293zbMath1185.68201OpenAlexW2096529083MaRDI QIDQ5189646

F. Zappa Nardelli, Scott Owens, Susmit Sarkar, Thomas Ridge, Rok Strniša, Peter Sewell, Gilles Peskine

Publication date: 17 March 2010

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0956796809990293

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

Related Items

Safe zero-cost coercions for Haskell ⋮ A formalized general theory of syntax with bindings ⋮ αCheck: A mechanized metatheory model checker ⋮ Unnamed Item ⋮ Romeo: A system for more flexible binding-safe programming ⋮ Dualized Simple Type Theory ⋮ Unnamed Item ⋮ Executable component-based semantics ⋮ A formalized general theory of syntax with bindings: extended version ⋮ Binding operators for nominal sets ⋮ A Formalization of the C99 Standard in HOL, Isabelle and Coq ⋮ General Bindings and Alpha-Equivalence in Nominal Isabelle ⋮ Implementing type systems for the IDE with Xsemantics ⋮ Lem: A Lightweight Tool for Heavyweight Semantics ⋮ Ott ⋮ Mechanized metatheory revisited ⋮ Dynamic structural operational semantics ⋮ Term-generic logic

Uses Software

• Coq
• Jakarta
• Isabelle/HOL
• TinkerType
• Haskell
• Proof General
• OCaml
• Freshml
• LaTeX

Cites Work

• Unnamed Item
• Nominal techniques in Isabelle/HOL
• An extension of system \(F\) with subtyping
• From syntactic theories to interpreters: Automating the proof of unique decomposition
• Mechanized semantics for the clight subset of the C language
• A syntactic theory of type generativity and sharing
• A Marriage of Rely/Guarantee and Separation Logic
• TinkerType: a language for playing with formal systems
• Acute: High-level programming language design for distributed computation