Implementing type systems for the IDE with Xsemantics

DOI10.1016/j.jlamp.2015.11.005zbMath1348.68030OpenAlexW2229705435MaRDI QIDQ739624

Lorenzo Bettini

Publication date: 18 August 2016

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlamp.2015.11.005

zbMATH Keywords

DSLsemanticsimplementationtype systemsEclipse

Mathematics Subject Classification ID

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

Uses Software

• Coq
• Isabelle
• Ott
• Stratego
• JastAdd
• ANTLR
• MontiCore
• LCF
• PLT Redex
• Featherweight Java
• Spoofax
• Neverlang
• Centaur
• K Prover
• Ruler

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• An overview of the K semantic framework
• Isabelle. A generic theorem prover
• The JastAdd system - modular extensible compiler construction
• A Theory of Name Resolution
• Ruler: Programming Type Rules
• Ott: Effective tool support for the working semanticist
• Scripting the type inference process

This page was built for publication: Implementing type systems for the IDE with Xsemantics