Travelled to:
1 × Brazil
1 × The Netherlands
Collaborated with:
D.Fridlender A.Abel T.Coquand A.Pardo Emmanuel Gunther M.Viera
Talks about:
type (5) algorithm (2) theori (2) check (2) internalist (1) singleton (1) construct (1) normalis (1) approach (1) modular (1)
Person: Miguel Pagano
DBLP: Pagano:Miguel
Contributed to:
Wrote 3 papers:
- TLCA-2013-FridlenderP #algorithm #evaluation #normalisation #type system
- A Type-Checking Algorithm for Martin-Löf Type Theory with Subtyping Based on Normalisation by Evaluation (DF, MP), pp. 140–155.
- TLCA-2009-AbelCP #algorithm #composition #proving #type system
- A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance (AA, TC, MP), pp. 5–19.
- PPDP-2018-PardoGPV #approach #compilation
- An Internalist Approach to Correct-by-Construction Compilers (AP, EG, MP, MV), p. 12.