Ott: Effective tool support for the working semanticist

DOI10.1017/S0956796809990293MaRDI QIDQ5189646zbMATH OpenOpenAlexFDO

Authors Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Tom Ridge, Susmit Sarkar, Rok Strniša

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)

Recommendations

• Ott, effective tool support for the working semanticist
• scientific article; zbMATH DE number 4050950
• An ontology segmentation tool
• scientific article; zbMATH DE number 1955882
• Reasoning support for Semantic Web ontology family languages using Alloy

Cites work

• A Marriage of Rely/Guarantee and Separation Logic
• A syntactic theory of type generativity and sharing
• Acute: High-level programming language design for distributed computation
• An extension of system \(F\) with subtyping
• From syntactic theories to interpreters: Automating the proof of unique decomposition
• scientific article; zbMATH DE number 1952947 (Why is no real title available?)
• Mechanized semantics for the clight subset of the C language
• Nominal techniques in Isabelle/HOL
• TinkerType: a language for playing with formal systems

Cited in

(26)

• Ott
• A formalized general theory of syntax with bindings
• Executable component-based semantics
• Binding operators for nominal sets
• A formalized general theory of syntax with bindings: extended version
• Mechanized metatheory revisited
• Dynamic structural operational semantics
• Term-generic logic
• Lem: reusable engineering of real-world semantics
• Dualized simple type theory
• Lem: a lightweight tool for heavyweight semantics
• Semantics engineering with PLT Redex
• αCheck: A mechanized metatheory model checker
• Reasoning about modular datatypes with Mendler induction
• Ott, effective tool support for the working semanticist
• A formalization of the C99 standard in HOL, Isabelle and Coq
• Romeo: a system for more flexible binding-safe programming
• Safe zero-cost coercions for Haskell
• General bindings and alpha-equivalence in Nominal Isabelle
• \(\eta\)-equivalence in core dependent Haskell
• Mechanized metatheory revisited: an extended abstract (invited paper)
• An open challenge problem repository for systems supporting binders
• The way we were: structural operational semantics research in perspective
• A simple blame calculus for explicit nulls
• Modular abstract syntax trees (MAST): substitution tensors with second-class sorts
• Implementing type systems for the IDE with Xsemantics

Describes a project that uses

Uses Software

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

This page was built for publication: Ott: Effective tool support for the working semanticist

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