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