JProver is a first-order intuitionistic theorem prover that creates sequent-style proof objects and can serve as a proof engine
in interactive proof assistants with expressive constructive logics. This paper gives a brief overview of JProver’s proof
technique, the generation of proof objects, and its integration into the Nuprl proof development system.