MetaPRL

MetaPRL is two things: it is a logical framework where multiple logics can be defined and related, and it is a system implementation with support for interactive proof and automated reasoning. A primary feature of MetaPRL is a semantic connection to programming languages, that allows the system to be used as a logical programming environment, where programs are constructed as a mixture of specifications, implementations, and verifications.


References in zbMATH (referenced in 22 articles )

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

1 2 next

  1. Constable, Robert; Bickford, Mark: Intuitionistic completeness of first-order logic (2014)
  2. Palmgren, Erik; Wilander, Olov: Constructing categories and setoids of setoids in type theory (2014)
  3. James, Perry R.; Chalin, Patrice: Faster and more complete extended static checking for the Java modeling language (2010)
  4. Rioboo, Renaud: Invariants for the FoCaL language (2009)
  5. Amjad, Hasan: Data compression for proof replay (2008)
  6. Constable, Robert L.; Moczydlowski, Wojciech: Extracting programs from constructive HOL proofs via IZF set-theoretic semantics (2008)
  7. Hickey, Jason; Nogin, Aleksey; Yu, Xin; Kopylov, Alexei: Practical reflection for sequent logics. (2007)
  8. Hickey, Jason; Nogin, Aleksey; Yu, Xin; Kopylov, Alexei: Practical reflection for sequent logics (2007)
  9. Kang, Eunsuk; Aagaard, Mark D.: Improving the usability of HOL through controlled automation tactics (2007)
  10. Aboul-Hosn, Kamal; Kozen, Dexter: KAT-ML: an interactive theorem prover for Kleene algebra with tests (2006)
  11. Allen, S.F.; Bickford, M.; Constable, R.L.; Eaton, R.; Kreitz, C.; Lorigo, L.; Moran, E.: Innovations in computational type theory using Nuprl (2006)
  12. Hickey, Jason; Nogin, Aleksey: Formal compiler construction in a logical framework (2006)
  13. Hickey, Jason; Nogin, Aleksey; Yu, Xin; Kopylov, Alexei: Mechanized meta-reasoning using a hybrid HOAS/de Bruijn representation and reflection (2006)
  14. Nogin, Aleksey; Kopylov, Alexei: Formalizing type operations using the ”Image” type constructor. (2006)
  15. Nogin, Aleksey; Kopylov, Alexei: Formalizing type operations using the “image” type constructor (2006)
  16. Hickey, Jason; Nogin, Aleksey: Extensible hierarchical tactic construction in a logical framework (2004)
  17. Kreitz, Christoph: Building reliable, high-performance networks with the Nuprl proof development system (2004)
  18. Granicz, Adam; Zimmerman, Daniel M.; Hickey, Jason: Rewriting UNITY (2003)
  19. Hickey, Jason; Nogin, Aleksey; Constable, Robert L.; Aydemir, Brian E.; Barzilay, Eli; Bryukhov, Yegor; Eaton, Richard; Granicz, Adam; Kopylov, Alexei; Kreitz, Christoph; Krupski, Vladimir N.; Lorigo, Lori; Schmitt, Stephan; Witty, Carl; Yu, Xin: MetaPRL -- a modular logical environment (2003)
  20. Nogin, Aleksey; Hickey, Jason: Sequent schema for derived rules (2002)

1 2 next