References

Avigad, J. and J. Harrison, 2014. Formally verified mathematics. Commun. ACM., 57: 66-75.
CrossRef  |  Direct Link  |  

Coquand, C., 1993. From semantics to rules: A machine assisted analysis. Proceedings of the International Workshop on Computer Science Logic, August 24-28, 1993, Springer, Berlin, Germany, ISBN:978-3-540-58277-9, pp: 91-105.

Coquand, C., 2002. A formalised proof of the soundness and completeness of a simply typed Lambda-calculus with explicit substitutions. Higher Order Symbolic Comput., 15: 57-90.
CrossRef  |  Direct Link  |  

Coquand, T., 1991. An Algorithm for Testing Conversion in Type Theory. In: Logical Frameworks, Huet, G. and G. Plotkin (Eds.). Cambridge University Press, Cambridge, UK., ISBN:9780521413008, pp: 255-279.

Ebert, P.A. and M. Rossberg, 2013. Gottlob Frege: Basic Laws of Arithmetic. Oxford University Press, Oxford, UK., ISBN:9780199281749,.

Frege, G., 1879. Begriffsschrift, Eine Der Arithmetischen Nachgebildete Formelsprache Des Reinen Denkens. Hachette Livre Bnf, Paris, France, ISBN-13: 978-2012525719, Pages: 106.

Herbelin, H. and G. Lee, 2009. Forcing-based Cut-elimination for Gentzen-style intuitionistic sequent calculus. Proceedings of the International Workshop on Logic, Language, Information and Computation, June 21-24, 2009, Springer, Berlin, Germany, ISBN:978-3-642-02260-9, pp: 209-217.

Herberlin, H., S. Kim and G. Lee, 2017. Formalizing the Meta-theory of firstorder predicate logic. J. Korean Math. Soc., 54: 1521-1536.

Ilik, D., G. Lee and H. Herbelin, 2010. Kripke models for classical logic. Ann. Pure Applied Logic, 161: 1367-1378.
CrossRef  |  

Kripke, S., 1963. Semantical considerations on modal and intuitionistic logic. Acta Philos. Fennica, 16: 83-94.

Kripke, S.A., 1959. A completeness theorem in modal logic. J. Symbolic Logic, 24: 1-14.
CrossRef  |  Direct Link  |  

Lee, G., H. Herbelinand S. Kim, 2016. When locally-named becomes nominal: Technical report. Under Consideration Publ. J. Funct. Program., 2016: 1-6.
Direct Link  |  

McKinna, J. and R. Pollack, 1993. Pure type systems formalized. Proceedings of the International Conference on Typed Lambda Calculi and Applications, March 16-18, 1993, Springer, Berlin, Germany, ISBN:978-3-540-56517-8, pp: 289-305.

McKinna, J. and R. Pollack, 1999. Some lambda calculus and type theory formalized. J. Autom. Reasoning, 23: 373-409.
CrossRef  |  Direct Link  |  

Troelstra, A.S. and V.D. Dalen, 1988. Constructivism in Mathematics: An Introduction. North Holland Publishing Company, New York, USA., ISBN:9780444703583, Pages: 879.