In fact, the Nqthm theorem prover [Boyer and Moore 1988] uses type information internally, even though the logic is untyped.
ACL2: An industrial strength version of Nqthm. In Proceedings of the Eleventh Annual Conference on Computer Assurance (COMPASS-96), pp.
For recent notable work, I focus on some significant theorem-proving systems: the geometry theorem provers of Chou (Chou, Gao, and Zhang 1994; Chou 1988); the Boyer and Moore (1988) interactive theorem prover NQTHM and its successor ACL2 (Kaufmann and Moore 1996); the rewrite rule laboratory (RRL) of Kaput and Zhang (1995); the resolution prover OTTER (McCune and Otter 1997; McCune 1994) and the equational logic prover EQP by McCune (1996); the interactive higher-order logic provers NUPRL (Constable et al.
(Such high-investment projects exist in software also, but such systems usually are so complex that formal verification for them is rare.) The ACL2 prover (Kaufmann and Moore 1996), the successor of NQTHM, recently was used interactively to obtain a formal proof of the correctness of the floating-point divide code for AMD's newest PENTIUM-like microprocessor.
The ability to tackle these real-world problems is primarily the result of the improved capabilities of interactive systems such as NQTHM, ACL2, PVS, NUPRL, HOL, COQ (Coquand and Huet [INRIA] 1988), and ISABELLE (Paulson [Cambridge] 1994).
However, many other systems now have user communities of their own, some sizable: NQTHM, ACL2, and RRL, for example, and the higher-order logic systems HOL, NUPRL, ISABELLE, PVS, COQ, and TPS.
Some systems that are partially successful in combining techniques are PVS, NQTHM, ACL2, HOL, EVES (Craigen et al.