Here's one paper covering the derivation of a typed functional LALR(1) parser in which derivations are given explicitly in symbolic language, while proofs are just prose claims that an inductive proof is similar to the derivation:
Here's one for the semantics of the Cedille functional language core in which proofs are given as key components in symbolic language with prose to to tie them together; all theorems, lemmas, etc are given symbolically.
https://arxiv.org/abs/1806.04709
And here's one introducing dependent intersection types (as used in Cedille) which references formal machine-checked proofs and only provides a sketch of the proof result in prose:
https://doi.org/10.1109/LICS.2003.1210048
(For the latter, actually finding the machine checked proof might be tricky: I didn't see it overtly cited and I didn't go looking).
Here's one paper covering the derivation of a typed functional LALR(1) parser in which derivations are given explicitly in symbolic language, while proofs are just prose claims that an inductive proof is similar to the derivation:
Here's one for the semantics of the Cedille functional language core in which proofs are given as key components in symbolic language with prose to to tie them together; all theorems, lemmas, etc are given symbolically.
And here's one introducing dependent intersection types (as used in Cedille) which references formal machine-checked proofs and only provides a sketch of the proof result in prose:
(For the latter, actually finding the machine checked proof might be tricky: I didn't see it overtly cited and I didn't go looking).