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 123 articles )

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

1 2 3 ... 5 6 7 next

  1. Lucas, Salvador; Gutiérrez, Raúl: Automatic synthesis of logical models for order-sorted first-order theories (2018)
  2. Lucas, Salvador; Meseguer, José; Gutiérrez, Raúl: The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors (2018)
  3. Lucas, Salvador; Meseguer, José: Dependency pairs for proving termination properties of conditional term rewriting systems (2017)
  4. Meseguer, José; Skeirik, Stephen: Equational formulas and pattern operations in initial order-sorted algebras (2017)
  5. Rabe, Florian: Morphism axioms (2017)
  6. Riesco, Adrián; Ogata, Kazuhiro; Futatsugi, Kokichi: A Maude environment for CafeOBJ (2017)
  7. Diaconescu, Răzvan: Functorial semantics of first-order views (2016)
  8. Lucas, Salvador; Meseguer, José: Normal forms and normal theories in conditional rewriting (2016)
  9. Clavel, Manuel; Durán, Francisco; Eker, Steven; Escobar, Santiago; Lincoln, Patrick; Martí-Oliet, Narciso; Talcott, Carolyn: Two decades of Maude (2015)
  10. Gutiérrez, Raúl; Lucas, Salvador: Function calls at frozen positions in termination of context-sensitive rewriting (2015)
  11. Meseguer, José; Skeirik, Stephen: Equational formulas and pattern operations in initial order-sorted algebras (2015)
  12. Rabe, Florian: Lax theory morphisms (2015)
  13. Alpuente, María; Escobar, Santiago; Espert, Javier; Meseguer, José: A modular order-sorted equational generalization algorithm (2014)
  14. Bertolissi, Clara; Fernández, Maribel: A metamodel of access control for distributed environments: applications and properties (2014)
  15. Bjørner, Dines: Domain endurants. An analysis and description process model (2014)
  16. Diaconescu, Răzvan: CafeOBJ traces (2014)
  17. Martins, Manuel A.; Madeira, Alexandre; Barbosa, Luís S.: The role of logical interpretations in program development (2014)
  18. Mossakowski, Till; Pawłowski, Wiesław; Sannella, Donald; Tarlecki, Andrzej: Parchments for CafeOBJ logics (2014)
  19. Nakamura, Masaki; Ogata, Kazuhiro; Futatsugi, Kokichi: Incremental proofs of termination, confluence and sufficient completeness of OBJ specifications (2014)
  20. Ogata, Kazuhiro; Futatsugi, Kokichi: Theorem proving based on proof scores for rewrite theory specifications of otss (2014)

1 2 3 ... 5 6 7 next