OBJ3 is a program specification and proof system based on order sorted equational logic. It has been successfully used for research and teaching in software design and specification, rapid prototyping, theorem proving, user interface design, and hardware verification, among other things. It was the first language to implement parameterized programming and its module system influenced the designs of the Ada, C++, and ML module systems. (Source: http://freecode.com/)

References in zbMATH (referenced in 98 articles )

Showing results 1 to 20 of 98.
Sorted by year (citations)

1 2 3 4 5 next

  1. Lucas, Salvador; Meseguer, José: Dependency pairs for proving termination properties of conditional term rewriting systems (2017)
  2. Meseguer, José; Skeirik, Stephen: Equational formulas and pattern operations in initial order-sorted algebras (2017)
  3. Riesco, Adrián; Ogata, Kazuhiro; Futatsugi, Kokichi: A Maude environment for CafeOBJ (2017)
  4. Diaconescu, Răzvan: Functorial semantics of first-order views (2016)
  5. Alpuente, María; Escobar, Santiago; Espert, Javier; Meseguer, José: A modular order-sorted equational generalization algorithm (2014)
  6. Bertolissi, Clara; Fernández, Maribel: A metamodel of access control for distributed environments: applications and properties (2014)
  7. Martins, Manuel A.; Madeira, Alexandre; Barbosa, Luís S.: The role of logical interpretations in program development (2014)
  8. Ţuţu, Ionuţ: Parameterisation for abstract structured specifications (2014)
  9. Rabe, Florian; Kohlhase, Michael: A scalable module system (2013)
  10. Diaconescu, Răzvan: An axiomatic approach to structuring specifications (2012)
  11. Futatsugi, Kokichi; Găină, Daniel; Ogata, Kazuhiro: Principles of proof scores in CafeOBJ (2012)
  12. Meseguer, José: Twenty years of rewriting logic (2012)
  13. Diaconescu, Răzvan; Ţuţu, Ionuţ: On the algebra of structured specifications (2011)
  14. Alarcón, Beatriz; Gutiérrez, Raúl; Lucas, Salvador: Context-sensitive dependency pairs (2010)
  15. Alpuente, M.; Escobar, S.; Gramlich, B.; Lucas, S.: On-demand strategy annotations revisited: an improved on-demand evaluation strategy (2010)
  16. Diaconescu, Răzvan: Quasi-Boolean encodings and conditionals in algebraic specification (2010)
  17. Durán, Francisco; Meseguer, José: A Church-Rosser checker tool for conditional order-sorted equational Maude specifications (2010)
  18. Roşu, Grigore; Şerbănuţă, Traian Florin: An overview of the K semantic framework (2010)
  19. Shankar, Natarajan: Rewriting, inference, and proof (2010)
  20. Alarcón, Beatriz; Lucas, Salvador: Using context-sensitive rewriting for proving innermost termination of rewriting (2009)

1 2 3 4 5 next